src/Pure/Isar/method.ML
changeset 19778 f0a318495ca4
parent 19482 9f11af8f7ef9
child 20030 e62913ef9d24
     1.1 --- a/src/Pure/Isar/method.ML	Mon Jun 05 21:54:23 2006 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Jun 05 21:54:24 2006 +0200
     1.3 @@ -219,14 +219,15 @@
     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 +fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
    1.11 +  if cond (Logic.strip_assums_concl prop)
    1.12 +  then Tactic.rtac rule i else no_tac);
    1.13  
    1.14  fun assm_tac ctxt =
    1.15    assume_tac APPEND'
    1.16    asm_tac (ProofContext.prems_of ctxt) APPEND'
    1.17 -  refl_tac;
    1.18 +  cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
    1.19 +  cond_rtac (can Logic.dest_term) Drule.termI;
    1.20  
    1.21  fun assumption_tac ctxt [] = assm_tac ctxt
    1.22    | assumption_tac _ [fact] = asm_tac [fact]