# HG changeset patch
# User wenzelm
# Date 1163620224 -3600
# Node ID c648e24fd7ee1fa9bb7f7fcced8a9093bfc2fdd6
# Parent  e571e84cbe89980e49e5946fe5775b5a2209c4f4
add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);

diff -r e571e84cbe89 -r c648e24fd7ee src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Nov 15 20:50:23 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Nov 15 20:50:24 2006 +0100
@@ -1771,13 +1771,13 @@
         |> snd;
     val (ctxt, (_, facts)) = activate_facts true (K I)
       (ProofContext.init pred_thy, axiomify predicate_axioms elemss');
-    val export = singleton (ProofContext.export_standard
-        (Assumption.add_view thy_ctxt predicate_statement ctxt) thy_ctxt);
+    val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
+    val export = singleton (ProofContext.export_standard view_ctxt thy_ctxt);
     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
     val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
     val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
     val axs' = map (Element.assume_witness pred_thy) stmt';
-    val ctxt' = ctxt |> ProofContext.theory (fn pred_thy => pred_thy
+    val loc_ctxt = pred_thy
       |> PureThy.note_thmss_qualified "" bname facts' |> snd
       |> declare_locale name
       |> put_locale name
@@ -1788,8 +1788,9 @@
         lparams = map #1 (params_of' body_elemss),
         term_syntax = [],
         regs = regs,
-        intros = intros});
-  in (name, ctxt') end;
+        intros = intros}
+      |> init name;
+  in (name, loc_ctxt) end;
 
 in