src/Pure/Isar/locale.ML

   let
     val wits = all_witnesses ctxt |> map Thm.varifyT;
     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
   [("intro_locales",
     Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),