From 31cc0ebb6a6662e72ca8de9838219942d7347eb6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 4 Feb 2016 15:44:54 -0800
Subject: [PATCH] fix(frontends/lean/structure_cmd): fixes #968

---
 src/frontends/lean/structure_cmd.cpp |  1 +
 tests/lean/run/968.lean              | 15 +++++++++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 tests/lean/run/968.lean

diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 1e514ccf2..ff4bfa8ca 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -605,6 +605,7 @@ struct structure_cmd_fn {
         expr tmp   = Pi(m_params, Pi(m_fields, dummy));
         collected_locals local_set;
         ::lean::collect_locals(tmp, local_set);
+        collect_annonymous_inst_implicit(m_p, local_set);
         sort_locals(local_set.get_collected(), m_p, locals);
     }
 
diff --git a/tests/lean/run/968.lean b/tests/lean/run/968.lean
new file mode 100644
index 000000000..1710d7348
--- /dev/null
+++ b/tests/lean/run/968.lean
@@ -0,0 +1,15 @@
+variables (A : Type) [inhabited A]
+
+definition f (a : A) : A := a
+
+check @f nat nat.is_inhabited
+
+structure foo :=
+(a : A)
+
+check @foo nat nat.is_inhabited
+
+inductive bla :=
+| mk : A → bla
+
+check @bla nat nat.is_inhabited