tuned;

--- a/src/Pure/Isar/locale.ML	Tue Jan 03 00:06:26 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Jan 03 00:06:28 2006 +0100
@@ -1691,7 +1691,6 @@
     val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
       if do_predicate then thy |> define_preds bname text elemss
       else (thy, (elemss, ([], [])));
-    val pred_ctxt = ProofContext.init pred_thy;
 
     fun axiomify axioms elemss =
       (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
@@ -1701,8 +1700,8 @@
                  in (axs2, ((id, Assumed axs1), elems)) end)
         |> snd;
     val (ctxt, (_, facts)) = activate_facts (K I)
-      (pred_ctxt, axiomify predicate_axioms elemss');
-    val export = ProofContext.export_view predicate_statement ctxt pred_ctxt;
+      (thy_ctxt, axiomify predicate_axioms 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) elemss'))
   in