Locale.init;

--- a/src/Pure/Isar/isar_cmd.ML	Fri Jan 27 19:03:08 2006 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Jan 27 19:03:09 2006 +0100
@@ -360,7 +360,7 @@
 
 fun enter_locale NONE = Toplevel.theory I
   | enter_locale (SOME loc) = Toplevel.theory_context (fn thy =>
-      (thy, #3 (Locale.read_context_statement (SOME loc) [] [] (ProofContext.init thy))));
+      (#2 (Locale.init (Locale.intern thy loc) thy), thy));
 
 fun present_text proof present loc (s, pos) = Toplevel.keep' (fn int => fn state =>
  (Toplevel.assert (can Toplevel.proof_of state = proof);

--- a/src/Pure/Isar/isar_output.ML	Fri Jan 27 19:03:08 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML	Fri Jan 27 19:03:09 2006 +0100
@@ -115,10 +115,10 @@
 
 fun args scan f src state : string =
   let
+    val thy = Toplevel.theory_of state;
     val ctxt0 =
       if ! locale = "" then Toplevel.body_context_of state
-      else #3 (Locale.read_context_statement (SOME (! locale)) [] []
-        (ProofContext.init (Toplevel.theory_of state)));
+      else #2 (Locale.init (Locale.intern thy (! locale)) thy);
     val (ctxt, x) = syntax scan src ctxt0;
   in f src ctxt x end;