Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified add_thmss;
authorwenzelm
Wed, 29 Nov 2006 23:28:11 +0100
changeset 21598 2b702007e7c8
parent 21597 0e7a441ac637
child 21599 f424d328090c
simplified add_thmss; mark predicate definitions as internal;
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- 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';
isabelle