1.1 --- a/src/Pure/Isar/method.ML	Thu Jan 01 22:20:29 2009 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Jan 01 22:57:42 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Pure/Isar/method.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Muenchen
     1.7  
     1.8  Isar proof methods.
     1.9 @@ -223,15 +222,9 @@
    1.10    if cond (Logic.strip_assums_concl prop)
    1.11    then Tactic.rtac rule i else no_tac);
    1.12  
    1.13 -fun legacy_tac st =
    1.14 -  (legacy_feature
    1.15 -      ("Implicit use of prems in assumption proof" ^ Position.str_of (Position.thread_data ()));
    1.16 -    all_tac st);
    1.17 -
    1.18  fun assm_tac ctxt =
    1.19    assume_tac APPEND'
    1.20    Goal.assume_rule_tac ctxt APPEND'
    1.21 -  (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K legacy_tac) APPEND'
    1.22    cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
    1.23    cond_rtac (can Logic.dest_term) Drule.termI;
    1.24