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