generic tactic Method.intros_tac

--- a/src/Pure/Isar/locale.ML	Fri Nov 02 18:53:00 2007 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Nov 02 18:53:01 2007 +0100
@@ -1955,9 +1955,7 @@
     val thy = ProofContext.theory_of ctxt;
     val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
   in
-    (ALLGOALS (Method.insert_tac facts THEN'
-        REPEAT_ALL_NEW (resolve_tac (wits @ intros)))
-      THEN Tactic.distinct_subgoals_tac) st
+    Method.intros_tac (wits @ intros) facts st
   end;
 
 val _ = Context.add_setup (Method.add_methods

--- a/src/Pure/Isar/method.ML	Fri Nov 02 18:53:00 2007 +0100
+++ b/src/Pure/Isar/method.ML	Fri Nov 02 18:53:01 2007 +0100
@@ -45,6 +45,7 @@
   val trace: Proof.context -> thm list -> unit
   val rule_tac: thm list -> thm list -> int -> tactic
   val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
+  val intros_tac: thm list -> thm list -> tactic
   val rule: thm list -> method
   val erule: int -> thm list -> method
   val drule: int -> thm list -> method
@@ -288,6 +289,14 @@
 end;
 
 
+(* intros_tac -- pervasive search spanned by intro rules *)
+
+fun intros_tac intros facts =
+  ALLGOALS (insert_tac facts THEN'
+      REPEAT_ALL_NEW (resolve_tac intros))
+    THEN Tactic.distinct_subgoals_tac;
+
+
 (* iprover -- intuitionistic proof search *)
 
 local