# HG changeset patch
# User haftmann
# Date 1136366911 -3600
# Node ID cf0edebe540c4ed24176601eb5dd00384c95e875
# Parent  0728c4c38b6239e4d5a55c13722505ab918a48ef
fix: reintroduced pred_ctxt in gen_add_locale

diff -r 0728c4c38b62 -r cf0edebe540c src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Jan 04 01:04:59 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Jan 04 10:28:31 2006 +0100
@@ -1718,8 +1718,9 @@
                    val (axs1, axs2) = splitAt (length ts, axs);
                  in (axs2, ((id, Assumed axs1), elems)) end)
         |> snd;
+    val pred_ctxt = ProofContext.init pred_thy;
     val (ctxt, (_, facts)) = activate_facts (K I)
-      (thy_ctxt, axiomify predicate_axioms ((op @) elemss'));
+      (pred_ctxt, axiomify predicate_axioms ((op @) elemss'));
     val export = ProofContext.export_view predicate_statement ctxt thy_ctxt;
     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
     val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) ((op @) elemss')))