# HG changeset patch
# User ballarin
# Date 1266260094 -3600
# Node ID eb1cc37bc8dbe0aad4d112981117233cbca2035a
# Parent  0880493627ca432786b267da1ee510a33d03422c
Removed obsolete function.

diff -r 0880493627ca -r eb1cc37bc8db src/Pure/Isar/locale.ML
--- 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