From 27c1d2f4fbcee4e4ebbd854e45889bdeb92d446e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 11 May 2017 15:58:47 +0200
Subject: [PATCH] fix(init/meta/interactive): simp: accept local refs as simp
 names

---
 library/init/meta/interactive.lean |  4 +++-
 tests/lean/run/1577.lean           | 17 +++++++++++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/1577.lean

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 52e8282171..90c48c929b 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -576,7 +576,9 @@ fail ("invalid simplification lemma '" ++ to_string n ++ "' (use command 'set_op
 private meta def simp_lemmas.resolve_and_add (s : simp_lemmas) (n : name) (ref : expr) : tactic simp_lemmas :=
 do
   p ← resolve_name n,
-  match p.to_raw_expr with
+  -- unpack local refs
+  let e := p.to_raw_expr.erase_annotations.get_app_fn.erase_annotations,
+  match e with
   | const n _           :=
     (do b ← is_valid_simp_lemma_cnst reducible n, guard b, save_const_type_info n ref, s.add_simp n)
     <|>
diff --git a/tests/lean/run/1577.lean b/tests/lean/run/1577.lean
new file mode 100644
index 0000000000..5f1738b4f3
--- /dev/null
+++ b/tests/lean/run/1577.lean
@@ -0,0 +1,17 @@
+section
+
+parameter T : Type
+
+def eqT : T -> T ->  Prop
+| t1 t2 := t1 = t2
+
+lemma sm : forall t1 t2,
+eqT t1 t2 ->
+t1 = t2 :=
+begin
+intros,
+simp [eqT] at a,
+assumption
+end
+
+end