# HG changeset patch
# User wenzelm
# Date 1230847062 -3600
# Node ID 2b845381ba6ae91712d01b7313e5f139b913a3ca
# Parent  df4300a1acd3ae70549c987794e0c30fb533ebc7
assumption/close: discontinued implicit prems;

diff -r df4300a1acd3 -r 2b845381ba6a src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jan 01 22:20:29 2009 +0100
+++ b/src/Pure/Isar/method.ML	Thu Jan 01 22:57:42 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/method.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Isar proof methods.
@@ -223,15 +222,9 @@
   if cond (Logic.strip_assums_concl prop)
   then Tactic.rtac rule i else no_tac);
 
-fun legacy_tac st =
-  (legacy_feature
-      ("Implicit use of prems in assumption proof" ^ Position.str_of (Position.thread_data ()));
-    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 legacy_tac) APPEND'
   cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
   cond_rtac (can Logic.dest_term) Drule.termI;