src/Pure/Thy/export_theory.ML

           in triple (list (pair string sort)) (list (pair string typ)) term end
       end;
 
     fun encode_axiom used t = encode_prop used ([], t);
 
-    val encode_fact_single = encode_prop Name.context o prop_of;
-    val encode_fact_multi = XML.Encode.list (encode_prop Name.context) o map prop_of;
+    val encode_fact = encode_prop Name.context;
+    val encode_fact_single = encode_fact o prop_of;
+    val encode_fact_multi = XML.Encode.list encode_fact o map prop_of;
 
     val _ =
       export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
         Theory.axiom_space (Theory.axioms_of thy);
     val _ =

         Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
 
 
     (* sort algebra *)
 
-    val {classrel, arities} =
-      Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
-        (#2 (#classes rep_tsig));
-
-    val encode_prop0 =
-      encode_axiom Name.context o Logic.varify_global;
-
-    val encode_classrel =
-      let open XML.Encode
-      in list (pair encode_prop0 (pair string string)) end;
-
-    val encode_arities =
-      let open XML.Encode Term_XML.Encode
-      in list (pair encode_prop0 (triple string (list sort) string)) end;
-
-    val export_classrel =
-      maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel;
-
-    val export_arities = map (`Logic.mk_arity) #> encode_arities;
+    local
+      val prop = encode_axiom Name.context o Logic.varify_global;
+
+      val encode_classrel =
+        let open XML.Encode
+        in list (pair prop (pair string string)) end;
+
+      val encode_arities =
+        let open XML.Encode Term_XML.Encode
+        in list (pair prop (triple string (list sort) string)) end;
+    in
+      val export_classrel =
+        maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel;
+
+      val export_arities = map (`Logic.mk_arity) #> encode_arities;
+
+      val {classrel, arities} =
+        Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
+          (#2 (#classes rep_tsig));
+
+    end;
 
     val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel);
     val _ = if null arities then () else export_body thy "arities" (export_arities arities);