src/Pure/Thy/export_theory.ML

 
     fun encode_axiom used prop =
       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 *)
 
     val export_standard_proofs = Options.default_bool @{system_option export_standard_proofs};