--- 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);