--- a/src/Pure/Isar/locale.ML Thu Nov 30 14:17:22 2006 +0100
+++ b/src/Pure/Isar/locale.ML Thu Nov 30 14:17:25 2006 +0100
@@ -1809,7 +1809,8 @@
val (ctxt, (_, facts)) = activate_facts true (K I)
(ProofContext.init pred_thy, axiomify predicate_axioms elemss');
val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
- val export = singleton (ProofContext.export_standard view_ctxt thy_ctxt);
+ val export = Goal.close_result o Goal.norm_result o
+ singleton (ProofContext.export view_ctxt thy_ctxt);
val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';