# HG changeset patch
# User wenzelm
# Date 1119298454 -7200
# Node ID 09d43301b195c6ef4ce09849afac4f4697054895
# Parent  2076b2e6ac58a151eaba129b4970c4d8fbd40c1a
refl_tac: avoid failure of unification, i.e. confusing trace msg;
get_thm(s): Name;

diff -r 2076b2e6ac58 -r 09d43301b195 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Jun 20 22:14:13 2005 +0200
+++ b/src/Pure/Isar/method.ML	Mon Jun 20 22:14:14 2005 +0200
@@ -311,10 +311,14 @@
 fun asm_tac ths =
   foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths);
 
+val refl_tac = SUBGOAL (fn (prop, i) =>
+  if can Logic.dest_equals (Logic.strip_assums_concl prop)
+  then Tactic.rtac Drule.reflexive_thm i else no_tac);
+
 fun assm_tac ctxt =
   assume_tac APPEND'
   asm_tac (ProofContext.prems_of ctxt) APPEND'
-  Tactic.rtac Drule.reflexive_thm;
+  refl_tac;
 
 fun assumption_tac ctxt [] = assm_tac ctxt
   | assumption_tac _ [fact] = asm_tac [fact]
@@ -487,10 +491,10 @@
 fun tactic txt ctxt = METHOD (fn facts =>
   (Context.use_mltext
     ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic = \
-     \let val thm = ProofContext.get_thm_closure ctxt o rpair NONE\n\
-     \  and thms = ProofContext.get_thms_closure ctxt o rpair NONE in\n"
-     ^ txt ^
-     "\nend in Method.set_tactic tactic end")
+       \let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\
+       \  and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n"
+       ^ txt ^
+       "\nend in Method.set_tactic tactic end")
     false NONE;
     Context.setmp (SOME (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts));