Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/export_theory.ML
changeset 70923 98d9b78b7f47
parent 70920 1e0ad25c94c8
child 70974 3ee90f831805 
--- a/src/Pure/Thy/export_theory.ML	Tue Oct 22 20:08:25 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Tue Oct 22 20:55:13 2019 +0200
@@ -242,8 +242,8 @@
       encode_prop (#1 (standard_prop used [] prop NONE));
 
     val _ =
-      export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
-        Theory.axiom_space (Theory.axioms_of thy);
+      export_entities "axioms" (K (SOME o encode_axiom Name.context))
+        Theory.axiom_space (Theory.all_axioms_of thy);
 
 
     (* theorems and proof terms *)
isabelle