src/Pure/Thy/export_theory.ML

         (Name_Space.dest_table (#types rep_tsig));
 
 
     (* consts *)
 
+    val consts = Sign.consts_of thy;
+    val encode_term = Term_XML.Encode.term consts;
+
     val encode_const =
       let open XML.Encode Term_XML.Encode in
         pair encode_syntax
           (pair (list string)
-            (pair typ (pair (option term) (pair bool (pair (list string) bool)))))
+            (pair typ (pair (option encode_term) (pair bool (pair (list string) bool)))))
       end;
 
     fun export_const c (T, abbrev) =
       let
         val syntax = get_syntax_const thy_ctxt c;
         val U = Logic.unvarifyT_global T;
         val U0 = Type.strip_sorts U;
         val recursion = primrec_types thy_ctxt (c, U);
         val abbrev' = abbrev
           |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts);
-        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0));
+        val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
         val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
       in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end;
 
     val _ =
       export_entities "consts" (SOME oo export_const) Sign.const_space
-        (#constants (Consts.dest (Sign.consts_of thy)));
+        (#constants (Consts.dest consts));
 
 
     (* axioms *)
 
     fun standard_prop used extra_shyps raw_prop raw_proof =

         val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
       in ((sorts @ typargs, args, prop), proof) end;
 
     val encode_prop =
       let open XML.Encode Term_XML.Encode
-      in triple (list (pair string sort)) (list (pair string typ)) term end;
+      in triple (list (pair string sort)) (list (pair string typ)) encode_term end;
 
     fun encode_axiom used prop =
       encode_prop (#1 (standard_prop used [] prop NONE));
 
     val _ =

         val (prop, proof) =
           standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME raw_proof);
       in
         (prop, (deps, proof)) |>
           let open XML.Encode Term_XML.Encode
-          in pair encode_prop (pair (list string) (option Proofterm.encode_full)) end
+          in pair encode_prop (pair (list string) (option (Proofterm.encode_full consts))) end
       end;
 
     fun buffer_export_thm (serial, thm_name) =
       let
         val markup = entity_markup_thm (serial, thm_name);

     fun encode_locale_dependency (dep: Locale.locale_dependency, subst) =
       (#source dep, (#target dep, (#prefix dep, subst))) |>
         let
           open XML.Encode Term_XML.Encode;
           val encode_subst =
-            pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) term));
+            pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) (term consts)));
         in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
 
     val _ =
       get_dependencies parents thy
       |> map_index (fn (i, dep) =>