--- 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