From 6134c8822a3075bb8ecd79afe6c99bd19b2c4f8a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 24 Apr 2015 15:08:58 -0700
Subject: [PATCH] fix(frontends/lean/util): assertion violation

fixes #559
---
 src/frontends/lean/util.cpp      |  6 ++++--
 tests/lean/559.lean              | 12 ++++++++++++
 tests/lean/559.lean.expected.out |  4 ++++
 3 files changed, 20 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/559.lean
 create mode 100644 tests/lean/559.lean.expected.out

diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 4b4c6dc72..050672536 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -126,8 +126,10 @@ void collect_locals(expr const & type, expr const & value, parser const & p, buf
     buffer<expr> include_vars;
     p.get_include_variables(include_vars);
     for (expr const & param : include_vars) {
-        collect_locals_ignoring_tactics(mlocal_type(param), ls);
-        ls.insert(param);
+        if (is_local(param)) {
+            collect_locals_ignoring_tactics(mlocal_type(param), ls);
+            ls.insert(param);
+        }
     }
     collect_locals_ignoring_tactics(type, ls);
     collect_locals_ignoring_tactics(value, ls);
diff --git a/tests/lean/559.lean b/tests/lean/559.lean
new file mode 100644
index 000000000..30d88237b
--- /dev/null
+++ b/tests/lean/559.lean
@@ -0,0 +1,12 @@
+import algebra.ordered_field
+open algebra
+section sequence_c
+
+  parameter Q : Type
+  parameter lof_Q : linear_ordered_field Q
+  definition to_lof [instance] : linear_ordered_field Q := lof_Q
+  include to_lof
+
+  theorem foo (a b : Q) : a + b = b + a := !add.comm
+
+end sequence_c
diff --git a/tests/lean/559.lean.expected.out b/tests/lean/559.lean.expected.out
new file mode 100644
index 000000000..eb852a62a
--- /dev/null
+++ b/tests/lean/559.lean.expected.out
@@ -0,0 +1,4 @@
+559.lean:10:28: error: failed to synthesize placeholder
+Q : Type,
+a b : Q
+⊢ has_add Q