Removed obsolete function.
authorballarin
Mon Feb 15 19:54:54 2010 +0100 (2010-02-15)
changeset 36094eb1cc37bc8db
parent 36093 0880493627ca
child 36095 059c3568fdc8
Removed obsolete function.
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Feb 15 01:34:08 2010 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Feb 15 19:54:54 2010 +0100
     1.3 @@ -566,10 +566,6 @@
     1.4  
     1.5  
     1.6  (* Tactic *)
     1.7 -fun intros_tac intros facts =
     1.8 -  (TRYALL (Method.insert_tac facts THEN'
     1.9 -      REPEAT_ALL_NEW (resolve_tac intros)) |> CHANGED)
    1.10 -    THEN Tactic.distinct_subgoals_tac;
    1.11  
    1.12  fun gen_intro_locales_tac intros_tac eager ctxt =
    1.13    intros_tac