author | ballarin |
Mon, 15 Feb 2010 19:54:54 +0100 | |
changeset 36094 | eb1cc37bc8db |
parent 36093 | 0880493627ca |
child 36095 | 059c3568fdc8 |
--- a/src/Pure/Isar/locale.ML Mon Feb 15 01:34:08 2010 +0100 +++ b/src/Pure/Isar/locale.ML Mon Feb 15 19:54:54 2010 +0100 @@ -566,10 +566,6 @@ (* Tactic *) -fun intros_tac intros facts = - (TRYALL (Method.insert_tac facts THEN' - REPEAT_ALL_NEW (resolve_tac intros)) |> CHANGED) - THEN Tactic.distinct_subgoals_tac; fun gen_intro_locales_tac intros_tac eager ctxt = intros_tac