From f2b175280781fb40da37deba2c73d160e39ee953 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 Mar 2015 18:04:52 -0700
Subject: [PATCH] fix(frontends/lean/parser): add workaround for #461

---
 src/frontends/lean/parser.cpp       |  2 +-
 tests/lean/errors.lean.expected.out |  3 ++-
 tests/lean/run/all_goals2.lean      | 20 ++++++++++++++++++++
 3 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/all_goals2.lean

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 7c1b1e86e..8a3c87a41 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1432,7 +1432,7 @@ expr parser::parse_tactic_led(expr left) {
         expr right = parse_tactic();
         return mk_app({save_pos(mk_constant(get_tactic_and_then_name()), p), left, right}, p);
     } else {
-        throw parser_error("invalid tactic expression", p);
+        return parse_led(left);
     }
 }
 
diff --git a/tests/lean/errors.lean.expected.out b/tests/lean/errors.lean.expected.out
index 51eb795a8..9d7966f81 100644
--- a/tests/lean/errors.lean.expected.out
+++ b/tests/lean/errors.lean.expected.out
@@ -1,6 +1,7 @@
 errors.lean:4:0: error: unknown identifier 'a'
 tst1 : nat → nat → nat
-errors.lean:12:12: error: invalid tactic expression
+errors.lean:12:2: error: function expected at
+  tactic.cases [tactic.expr add] tactic.expr_list.nil
 errors.lean:22:12: error: unknown identifier 'b'
 tst3 A : A → A → A
 foo.tst1 : ℕ → ℕ → ℕ
diff --git a/tests/lean/run/all_goals2.lean b/tests/lean/run/all_goals2.lean
new file mode 100644
index 000000000..bbbf02b60
--- /dev/null
+++ b/tests/lean/run/all_goals2.lean
@@ -0,0 +1,20 @@
+import data.nat
+open nat
+
+attribute nat.add [unfold-c 2]
+attribute nat.rec_on [unfold-c 2]
+
+namespace tactic
+  definition then_all (t1 t2 : tactic) : tactic :=
+  focus (t1 ; all_goals t2)
+  infixl `;;`:15 := tactic.then_all
+end tactic
+
+open tactic
+example (a b c : nat) : (a + 0 = 0 + a ∧ b + 0 = 0 + b) ∧ c = c :=
+
+begin
+  apply and.intro,
+  apply and.intro ;; (esimp{of_num}; state; rewrite zero_add),
+  apply rfl
+end