refl_tac: avoid failure of unification, i.e. confusing trace msg;
authorwenzelm
Mon Jun 20 22:14:14 2005 +0200 (2005-06-20)
changeset 1650009d43301b195
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
     1.1 --- a/src/Pure/Isar/method.ML	Mon Jun 20 22:14:13 2005 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Jun 20 22:14:14 2005 +0200
     1.3 @@ -311,10 +311,14 @@
     1.4  fun asm_tac ths =
     1.5    foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths);
     1.6  
     1.7 +val refl_tac = SUBGOAL (fn (prop, i) =>
     1.8 +  if can Logic.dest_equals (Logic.strip_assums_concl prop)
     1.9 +  then Tactic.rtac Drule.reflexive_thm i else no_tac);
    1.10 +
    1.11  fun assm_tac ctxt =
    1.12    assume_tac APPEND'
    1.13    asm_tac (ProofContext.prems_of ctxt) APPEND'
    1.14 -  Tactic.rtac Drule.reflexive_thm;
    1.15 +  refl_tac;
    1.16  
    1.17  fun assumption_tac ctxt [] = assm_tac ctxt
    1.18    | assumption_tac _ [fact] = asm_tac [fact]
    1.19 @@ -487,10 +491,10 @@
    1.20  fun tactic txt ctxt = METHOD (fn facts =>
    1.21    (Context.use_mltext
    1.22      ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic = \
    1.23 -     \let val thm = ProofContext.get_thm_closure ctxt o rpair NONE\n\
    1.24 -     \  and thms = ProofContext.get_thms_closure ctxt o rpair NONE in\n"
    1.25 -     ^ txt ^
    1.26 -     "\nend in Method.set_tactic tactic end")
    1.27 +       \let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\
    1.28 +       \  and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n"
    1.29 +       ^ txt ^
    1.30 +       "\nend in Method.set_tactic tactic end")
    1.31      false NONE;
    1.32      Context.setmp (SOME (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts));
    1.33