refl_tac: avoid failure of unification, i.e. confusing trace msg;
authorwenzelm
Mon, 20 Jun 2005 22:14:14 +0200
changeset 16500 09d43301b195
parent 16499 2076b2e6ac58
child 16501 fec0cf020bad
refl_tac: avoid failure of unification, i.e. confusing trace msg; get_thm(s): Name;
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));