# HG changeset patch
# User wenzelm
# Date 1164839291 -3600
# Node ID 2b702007e7c83aaf99c1961f3845974060c89c4a
# Parent  0e7a441ac637b2baf20ace95503138d35a445b72
simplified add_thmss;
mark predicate definitions as internal;

diff -r 0e7a441ac637 -r 2b702007e7c8 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Nov 29 23:28:10 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Nov 29 23:28:11 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 = singleton (ProofContext.export_standard view_ctxt thy_ctxt);
+    val export = Drule.local_standard 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';