--- a/src/Pure/Isar/locale.ML Wed Nov 29 23:28:13 2006 +0100
+++ b/src/Pure/Isar/locale.ML Wed Nov 29 23:33:09 2006 +0100
@@ -1809,7 +1809,7 @@
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 = Drule.local_standard o singleton (ProofContext.export view_ctxt thy_ctxt);
+ val export = singleton (ProofContext.export_standard 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';