fix: reintroduced pred_ctxt in gen_add_locale
authorhaftmann
Wed, 04 Jan 2006 10:28:31 +0100
changeset 18569 cf0edebe540c
parent 18568 0728c4c38b62
child 18570 ffce25f9aa7f
fix: reintroduced pred_ctxt in gen_add_locale
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')))