# HG changeset patch
# User wenzelm
# Date 1181855080 -7200
# Node ID 15fb6637690ea0a5bda339d9f8be703566e57141
# Parent  474ff28210c0e59adf8ecbbd2b636509a2f0fcdf
method assumption: uniform treatment of prems as legacy feature;

diff -r 474ff28210c0 -r 15fb6637690e src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jun 14 23:04:39 2007 +0200
+++ b/src/Pure/Isar/method.ML	Thu Jun 14 23:04:40 2007 +0200
@@ -219,27 +219,27 @@
   if cond (Logic.strip_assums_concl prop)
   then Tactic.rtac rule i else no_tac);
 
-fun assm_tac warn_tac ctxt =
+fun legacy_tac ctxt st =
+  (legacy_feature ("implicit use of prems in assumption proof" ^ ContextPosition.str_of ctxt);
+    all_tac st);
+
+fun assm_tac ctxt =
   assume_tac APPEND'
   Goal.assume_rule_tac ctxt APPEND'
-  (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K warn_tac) APPEND'
+  (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K (legacy_tac ctxt)) APPEND'
   cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
   cond_rtac (can Logic.dest_term) Drule.termI;
 
-fun legacy_tac ctxt st =
-  (legacy_feature ("implicit use of prems at end of proof" ^ ContextPosition.str_of ctxt);
-    all_tac st);
-
 in
 
 fun assumption ctxt = METHOD (HEADGOAL o
-  (fn [] => assm_tac all_tac ctxt
+  (fn [] => assm_tac ctxt
     | [fact] => solve_tac [fact]
     | _ => K no_tac));
 
 fun close immed ctxt = METHOD (K
   (FILTER Thm.no_prems
-    ((if immed then ALLGOALS (assm_tac (legacy_tac ctxt) ctxt) else all_tac) THEN flexflex_tac)));
+    ((if immed then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac)));
 
 end;