diff -r 837f1b10722c -r 0c9650664d47 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Jul 04 15:30:30 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue Jul 04 15:45:59 2006 +0200
@@ -132,7 +132,7 @@
 fun init_i NONE thy = ProofContext.init thy
   | init_i (SOME loc) thy =
       thy
-      |> Locale.init loc
+      |> (fn thy => ([], Locale.init loc thy))
       ||>> ProofContext.inferred_fixes
       |> (fn ((view, params), ctxt) => Data.put
           {locale = SOME (loc, (view, ctxt)),
@@ -216,7 +216,7 @@
     (case locale_of ctxt of
       NONE => theory_result (PureThy.note_thmss_i kind (Attrib.map_facts attrib facts'))
     | SOME (loc, _) =>
-        locale_result (apfst #1 o Locale.add_thmss kind loc facts'))
+        locale_result (apfst #1 o (fn (_, ctxt) => Locale.add_thmss kind loc facts' ctxt)))
     ||> (#2 o ProofContext.note_thmss_i (Attrib.map_facts attrib facts))
   end;