method assumption: uniform treatment of prems as legacy feature;
authorwenzelm
Thu Jun 14 23:04:40 2007 +0200 (2007-06-14)
changeset 2339515fb6637690e
parent 23394 474ff28210c0
child 23396 6d72ababc58f
method assumption: uniform treatment of prems as legacy feature;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Thu Jun 14 23:04:39 2007 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Jun 14 23:04:40 2007 +0200
     1.3 @@ -219,27 +219,27 @@
     1.4    if cond (Logic.strip_assums_concl prop)
     1.5    then Tactic.rtac rule i else no_tac);
     1.6  
     1.7 -fun assm_tac warn_tac ctxt =
     1.8 +fun legacy_tac ctxt st =
     1.9 +  (legacy_feature ("implicit use of prems in assumption proof" ^ ContextPosition.str_of ctxt);
    1.10 +    all_tac st);
    1.11 +
    1.12 +fun assm_tac ctxt =
    1.13    assume_tac APPEND'
    1.14    Goal.assume_rule_tac ctxt APPEND'
    1.15 -  (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K warn_tac) APPEND'
    1.16 +  (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K (legacy_tac ctxt)) APPEND'
    1.17    cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
    1.18    cond_rtac (can Logic.dest_term) Drule.termI;
    1.19  
    1.20 -fun legacy_tac ctxt st =
    1.21 -  (legacy_feature ("implicit use of prems at end of proof" ^ ContextPosition.str_of ctxt);
    1.22 -    all_tac st);
    1.23 -
    1.24  in
    1.25  
    1.26  fun assumption ctxt = METHOD (HEADGOAL o
    1.27 -  (fn [] => assm_tac all_tac ctxt
    1.28 +  (fn [] => assm_tac ctxt
    1.29      | [fact] => solve_tac [fact]
    1.30      | _ => K no_tac));
    1.31  
    1.32  fun close immed ctxt = METHOD (K
    1.33    (FILTER Thm.no_prems
    1.34 -    ((if immed then ALLGOALS (assm_tac (legacy_tac ctxt) ctxt) else all_tac) THEN flexflex_tac)));
    1.35 +    ((if immed then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac)));
    1.36  
    1.37  end;
    1.38