diff --git a/src/Pure/PIDE/xml.ML b/src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML
+++ b/src/Pure/PIDE/xml.ML
@@ -1,417 +1,424 @@
 (*  Title:      Pure/PIDE/xml.ML
     Author:     David Aspinall
     Author:     Stefan Berghofer
     Author:     Makarius
 
 Untyped XML trees and representation of ML values.
 *)
 
 signature XML_DATA_OPS =
 sig
   type 'a A
   type 'a T
   type 'a V
   type 'a P
   val int_atom: int A
   val bool_atom: bool A
   val unit_atom: unit A
   val properties: Properties.T T
   val string: string T
   val int: int T
   val bool: bool T
   val unit: unit T
   val pair: 'a T -> 'b T -> ('a * 'b) T
   val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
   val list: 'a T -> 'a list T
   val option: 'a T -> 'a option T
   val variant: 'a V list -> 'a T
 end;
 
 signature XML =
 sig
   type attributes = (string * string) list
   datatype tree =
       Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
   val blob: string list -> body
+  val is_empty: tree -> bool
+  val is_empty_body: body -> bool
   val xml_elemN: string
   val xml_nameN: string
   val xml_bodyN: string
   val wrap_elem: ((string * attributes) * tree list) * tree list -> tree
   val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
   val add_content: tree -> Buffer.T -> Buffer.T
   val content_of: body -> string
   val trim_blanks: body -> body
   val header: string
   val text: string -> string
   val element: string -> attributes -> string list -> string
   val output_markup: Markup.T -> Markup.output
   val string_of: tree -> string
   val pretty: int -> tree -> Pretty.T
   val output: tree -> BinIO.outstream -> unit
   val parse_comments: string list -> unit * string list
   val parse_string : string -> string option
   val parse_element: string list -> tree * string list
   val parse_document: string list -> tree * string list
   val parse: string -> tree
   exception XML_ATOM of string
   exception XML_BODY of body
   structure Encode:
   sig
     include XML_DATA_OPS
     val tree: tree T
   end
   structure Decode:
   sig
     include XML_DATA_OPS
     val tree: tree T
   end
 end;
 
 structure XML: XML =
 struct
 
 (** XML trees **)
 
 open Output_Primitives.XML;
 
 val blob = map Text;
 
+fun is_empty (Text "") = true
+  | is_empty _ = false;
+
+val is_empty_body = forall is_empty;
+
 
 (* wrapped elements *)
 
 val xml_elemN = "xml_elem";
 val xml_nameN = "xml_name";
 val xml_bodyN = "xml_body";
 
 fun wrap_elem (((a, atts), body1), body2) =
   Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
 
 fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', atts'), body1) :: body2)) =
       if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN andalso null atts'
       then SOME (((a, atts), body1), body2) else NONE
   | unwrap_elem _ = NONE;
 
 
 (* text content *)
 
 fun add_content tree =
   (case unwrap_elem tree of
     SOME (_, ts) => fold add_content ts
   | NONE =>
       (case tree of
         Elem (_, ts) => fold add_content ts
       | Text s => Buffer.add s));
 
 fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
 
 
 (* trim blanks *)
 
 fun trim_blanks trees =
   trees |> maps
     (fn Elem (markup, body) => [Elem (markup, trim_blanks body)]
       | Text s =>
           let val s' = s |> raw_explode |> trim Symbol.is_blank |> implode;
           in if s' = "" then [] else [Text s'] end);
 
 
 
 (** string representation **)
 
 val header = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n";
 
 
 (* escaped text *)
 
 fun decode "&lt;" = "<"
   | decode "&gt;" = ">"
   | decode "&amp;" = "&"
   | decode "&apos;" = "'"
   | decode "&quot;" = "\""
   | decode c = c;
 
 fun encode "<" = "&lt;"
   | encode ">" = "&gt;"
   | encode "&" = "&amp;"
   | encode "'" = "&apos;"
   | encode "\"" = "&quot;"
   | encode c = c;
 
 val text = translate_string encode;
 
 
 (* elements *)
 
 fun elem name atts =
   space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
 
 fun element name atts body =
   let val b = implode body in
     if b = "" then enclose "<" "/>" (elem name atts)
     else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
   end;
 
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
   else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
 
 
 (* output *)
 
 fun buffer_of depth tree =
   let
     fun traverse _ (Elem ((name, atts), [])) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
       | traverse d (Elem ((name, atts), ts)) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
           traverse_body d ts #>
           Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
       | traverse _ (Text s) = Buffer.add (text s)
     and traverse_body 0 _ = Buffer.add "..."
       | traverse_body d ts = fold (traverse (d - 1)) ts;
   in Buffer.empty |> traverse depth tree end;
 
 val string_of = Buffer.content o buffer_of ~1;
 val output = Buffer.output o buffer_of ~1;
 
 fun pretty depth tree =
   Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
 
 val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
 
 
 
 (** XML parsing **)
 
 local
 
 fun err msg (xs, _) =
   fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
 
 fun ignored _ = [];
 
 fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
 fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
 val parse_name = Scan.one name_start_char ::: Scan.many name_char;
 
 val blanks = Scan.many Symbol.is_blank;
 val special = $$ "&" ^^ (parse_name >> implode) ^^ $$ ";" >> decode;
 val regular = Scan.one Symbol.not_eof;
 fun regular_except x = Scan.one (fn c => Symbol.not_eof c andalso c <> x);
 
 val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
 
 val parse_cdata =
   Scan.this_string "<![CDATA[" |--
   (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
   Scan.this_string "]]>";
 
 val parse_att =
   ((parse_name >> implode) --| (blanks -- $$ "=" -- blanks)) --
   (($$ "\"" || $$ "'") :|-- (fn s =>
     (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
 
 val parse_comment =
   Scan.this_string "<!--" --
   Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
   Scan.this_string "-->" >> ignored;
 
 val parse_processing_instruction =
   Scan.this_string "<?" --
   Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
   Scan.this_string "?>" >> ignored;
 
 val parse_doctype =
   Scan.this_string "<!DOCTYPE" --
   Scan.repeat (Scan.unless ($$ ">") regular) --
   $$ ">" >> ignored;
 
 val parse_misc =
   Scan.one Symbol.is_blank >> ignored ||
   parse_processing_instruction ||
   parse_comment;
 
 val parse_optional_text =
   Scan.optional (parse_chars >> (single o Text)) [];
 
 in
 
 val parse_comments =
   blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
 
 val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
 
 fun parse_content xs =
   (parse_optional_text @@@
     Scan.repeats
       ((parse_element >> single ||
         parse_cdata >> (single o Text) ||
         parse_processing_instruction ||
         parse_comment)
       @@@ parse_optional_text)) xs
 
 and parse_element xs =
   ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
     (fn (name, _) =>
       !! (err (fn () => "Expected > or />"))
        ($$ "/" -- $$ ">" >> ignored ||
         $$ ">" |-- parse_content --|
           !! (err (fn () => "Expected </" ^ implode name ^ ">"))
               ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
     >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
 
 val parse_document =
   (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
   |-- parse_element;
 
 fun parse s =
   (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
       (blanks |-- parse_document --| blanks))) (raw_explode s) of
     (x, []) => x
   | (_, ys) => error ("XML parsing error: unprocessed input\n" ^ Symbol.beginning 100 ys));
 
 end;
 
 
 
 (** XML as data representation language **)
 
 exception XML_ATOM of string;
 exception XML_BODY of tree list;
 
 
 structure Encode =
 struct
 
 type 'a A = 'a -> string;
 type 'a T = 'a -> body;
 type 'a V = 'a -> string list * body;
 type 'a P = 'a -> string list;
 
 
 (* atomic values *)
 
 fun int_atom i = Value.print_int i;
 
 fun bool_atom false = "0"
   | bool_atom true = "1";
 
 fun unit_atom () = "";
 
 
 (* structural nodes *)
 
 fun node ts = Elem ((":", []), ts);
 
 fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
 
 fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
 
 
 (* representation of standard types *)
 
 fun tree (t: tree) = [t];
 
 fun properties props = [Elem ((":", props), [])];
 
 fun string "" = []
   | string s = [Text s];
 
 val int = string o int_atom;
 
 val bool = string o bool_atom;
 
 val unit = string o unit_atom;
 
 fun pair f g (x, y) = [node (f x), node (g y)];
 
 fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
 
 fun list f xs = map (node o f) xs;
 
 fun option _ NONE = []
   | option f (SOME x) = [node (f x)];
 
 fun variant fs x =
   [tagged (the (get_index (fn f => SOME (f x) handle General.Match => NONE) fs))];
 
 end;
 
 
 structure Decode =
 struct
 
 type 'a A = string -> 'a;
 type 'a T = body -> 'a;
 type 'a V = string list * body -> 'a;
 type 'a P = string list -> 'a;
 
 
 (* atomic values *)
 
 fun int_atom s =
   Value.parse_int s
     handle Fail _ => raise XML_ATOM s;
 
 fun bool_atom "0" = false
   | bool_atom "1" = true
   | bool_atom s = raise XML_ATOM s;
 
 fun unit_atom "" = ()
   | unit_atom s = raise XML_ATOM s;
 
 
 (* structural nodes *)
 
 fun node (Elem ((":", []), ts)) = ts
   | node t = raise XML_BODY [t];
 
 fun vector atts =
   map_index (fn (i, (a, x)) => if int_atom a = i then x else raise XML_ATOM a) atts;
 
 fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
   | tagged t = raise XML_BODY [t];
 
 
 (* representation of standard types *)
 
 fun tree [t] = t
   | tree ts = raise XML_BODY ts;
 
 fun properties [Elem ((":", props), [])] = props
   | properties ts = raise XML_BODY ts;
 
 fun string [] = ""
   | string [Text s] = s
   | string ts = raise XML_BODY ts;
 
 val int = int_atom o string;
 
 val bool = bool_atom o string;
 
 val unit = unit_atom o string;
 
 fun pair f g [t1, t2] = (f (node t1), g (node t2))
   | pair _ _ ts = raise XML_BODY ts;
 
 fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
   | triple _ _ _ ts = raise XML_BODY ts;
 
 fun list f ts = map (f o node) ts;
 
 fun option _ [] = NONE
   | option f [t] = SOME (f (node t))
   | option _ ts = raise XML_BODY ts;
 
 fun variant fs [t] =
       let
         val (tag, (xs, ts)) = tagged t;
         val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
       in f (xs, ts) end
   | variant _ ts = raise XML_BODY ts;
 
 end;
 
 end;
diff --git a/src/Pure/Thy/export_theory.ML b/src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML
+++ b/src/Pure/Thy/export_theory.ML
@@ -1,420 +1,420 @@
 (*  Title:      Pure/Thy/export_theory.ML
     Author:     Makarius
 
 Export foundational theory content and locale/class structure.
 *)
 
 signature EXPORT_THEORY =
 sig
   val setup_presentation: (Thy_Info.presentation_context -> theory -> unit) -> unit
   val export_body: theory -> string -> XML.body -> unit
 end;
 
 structure Export_Theory: EXPORT_THEORY =
 struct
 
 (* approximative syntax *)
 
 val get_syntax = Syntax.get_approx o Proof_Context.syn_of;
 fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type;
 fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const;
 fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed;
 
 fun get_syntax_param ctxt loc x =
   let val thy = Proof_Context.theory_of ctxt in
     if Class.is_class thy loc then
       (case AList.lookup (op =) (Class.these_params thy [loc]) x of
         NONE => NONE
       | SOME (_, (c, _)) => get_syntax_const ctxt c)
     else get_syntax_fixed ctxt x
   end;
 
 val encode_syntax =
   XML.Encode.variant
    [fn NONE => ([], []),
     fn SOME (Syntax.Prefix delim) => ([delim], []),
     fn SOME (Syntax.Infix {assoc, delim, pri}) =>
       let
         val ass =
           (case assoc of
             Printer.No_Assoc => 0
           | Printer.Left_Assoc => 1
           | Printer.Right_Assoc => 2);
         open XML.Encode Term_XML.Encode;
       in ([], triple int string int (ass, delim, pri)) end];
 
 
 (* free variables: not declared in the context *)
 
 val is_free = not oo Name.is_declared;
 
 fun add_frees used =
   fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I);
 
 fun add_tfrees used =
   (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
 
 
 (* spec rules *)
 
 fun primrec_types ctxt const =
   Spec_Rules.retrieve ctxt (Const const)
   |> get_first
     (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME (types, false)
       | (Spec_Rules.Equational (Spec_Rules.Primcorec types), _) => SOME (types, true)
       | _ => NONE)
   |> the_default ([], false);
 
 
 (* locales content *)
 
 fun locale_content thy loc =
   let
     val ctxt = Locale.init loc thy;
     val args =
       Locale.params_of thy loc
       |> map (fn ((x, T), _) => ((x, T), get_syntax_param ctxt loc x));
     val axioms =
       let
         val (asm, defs) = Locale.specification_of thy loc;
         val cprops = map (Thm.cterm_of ctxt) (the_list asm @ defs);
         val (intro1, intro2) = Locale.intros_of thy loc;
         val intros_tac = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2) [];
         val res =
           Goal.init (Conjunction.mk_conjunction_balanced cprops)
           |> (ALLGOALS Goal.conjunction_tac THEN intros_tac)
           |> try Seq.hd;
       in
         (case res of
           SOME goal => Thm.prems_of goal
         | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
       end;
     val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);
   in {typargs = typargs, args = args, axioms = axioms} end;
 
 fun get_locales thy =
   Locale.get_locales thy |> map_filter (fn loc =>
     if Experiment.is_experiment thy loc then NONE else SOME (loc, ()));
 
 fun get_dependencies prev_thys thy =
   Locale.dest_dependencies prev_thys thy |> map_filter (fn dep =>
     if Experiment.is_experiment thy (#source dep) orelse
       Experiment.is_experiment thy (#target dep) then NONE
     else
       let
         val (type_params, params) = Locale.parameters_of thy (#source dep);
         val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
         val substT =
           typargs |> map_filter (fn v =>
             let
               val T = TFree v;
               val T' = Morphism.typ (#morphism dep) T;
             in if T = T' then NONE else SOME (v, T') end);
         val subst =
           params |> map_filter (fn (v, _) =>
             let
               val t = Free v;
               val t' = Morphism.term (#morphism dep) t;
             in if t aconv t' then NONE else SOME (v, t') end);
       in SOME (dep, (substT, subst)) end);
 
 
 (* general setup *)
 
 fun setup_presentation f =
   Theory.setup (Thy_Info.add_presentation (fn context => fn thy =>
     if Options.bool (#options context) "export_theory" then f context thy else ()));
 
 fun export_body thy name body =
-  if null body then ()
+  if XML.is_empty_body body then ()
   else Export.export thy (Path.binding0 (Path.make ["theory", name])) body;
 
 
 (* presentation *)
 
 val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
   let
     val parents = Theory.parents_of thy;
     val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
 
     val thy_ctxt = Proof_Context.init_global thy;
 
 
     (* entities *)
 
     fun make_entity_markup name xname pos serial =
       let
         val props =
           Position.offset_properties_of (adjust_pos pos) @
           Position.id_properties_of pos @
           Markup.serial_properties serial;
       in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
 
     fun entity_markup space name =
       let
         val xname = Name_Space.extern_shortest thy_ctxt space name;
         val {serial, pos, ...} = Name_Space.the_entry space name;
       in make_entity_markup name xname pos serial end;
 
     fun export_entities export_name export get_space decls =
       let
         val parent_spaces = map get_space parents;
         val space = get_space thy;
       in
         (decls, []) |-> fold (fn (name, decl) =>
           if exists (fn space => Name_Space.declared space name) parent_spaces then I
           else
             (case export name decl of
               NONE => I
             | SOME body =>
                 cons (#serial (Name_Space.the_entry space name),
                   XML.Elem (entity_markup space name, body))))
         |> sort (int_ord o apply2 #1) |> map #2
         |> export_body thy export_name
       end;
 
 
     (* types *)
 
     val encode_type =
       let open XML.Encode Term_XML.Encode
       in triple encode_syntax (list string) (option typ) end;
 
     fun export_type c (Type.LogicalType n) =
           SOME (encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
       | export_type c (Type.Abbreviation (args, U, false)) =
           SOME (encode_type (get_syntax_type thy_ctxt c, args, SOME U))
       | export_type _ _ = NONE;
 
     val _ =
       export_entities "types" export_type Sign.type_space
         (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 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 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 consts));
 
 
     (* axioms *)
 
     fun standard_prop used extra_shyps raw_prop raw_proof =
       let
         val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof);
         val args = rev (add_frees used prop []);
         val typargs = rev (add_tfrees used prop []);
         val used_typargs = fold (Name.declare o #1) typargs used;
         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)) encode_term end;
 
     fun encode_axiom used prop =
       encode_prop (#1 (standard_prop used [] prop NONE));
 
     val _ =
       export_entities "axioms" (K (SOME o encode_axiom Name.context))
         Theory.axiom_space (Theory.all_axioms_of thy);
 
 
     (* theorems and proof terms *)
 
     val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps;
 
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
     fun proof_boxes thm thm_id =
       let
         val selection =
          {included = Proofterm.this_id (SOME thm_id),
           excluded = is_some o lookup_thm_id};
         val boxes =
           map (Proofterm.thm_header_id o #1) (Proofterm.proof_boxes selection [Thm.proof_of thm])
             handle Proofterm.MIN_PROOF () => Thm_Deps.thm_boxes selection [thm]
      in boxes @ [thm_id] end;
 
     fun expand_name thm_id (header: Proofterm.thm_header) =
       if #serial header = #serial thm_id then ""
       else
         (case lookup_thm_id (Proofterm.thm_header_id header) of
           NONE => ""
         | SOME thm_name => Thm_Name.print thm_name);
 
     fun entity_markup_thm (serial, (name, i)) =
       let
         val space = Facts.space_of (Global_Theory.facts_of thy);
         val xname = Name_Space.extern_shortest thy_ctxt space name;
         val {pos, ...} = Name_Space.the_entry space name;
       in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
 
     fun encode_thm thm_id raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
         val thm = clean_thm (Thm.unconstrainT raw_thm);
         val boxes = proof_boxes thm thm_id;
 
         val proof0 =
           if Proofterm.export_standard_enabled () then
             Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm
           else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm
           else MinProof;
         val (prop, SOME proof) =
           standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0);
         val _ =
           if Proofterm.export_proof_boxes_required thy
           then Proofterm.export_proof_boxes [proof] else ();
       in
         (prop, (deps, (boxes, proof))) |>
           let
             open XML.Encode Term_XML.Encode;
             fun encode_box {serial, theory_name} = pair int string (serial, theory_name);
             val encode_proof = Proofterm.encode_standard_proof consts;
           in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end
       end;
 
     fun export_thm (thm_id, thm_name) =
       let
         val markup = entity_markup_thm (#serial thm_id, thm_name);
         val thm = Global_Theory.get_thm_name thy (thm_name, Position.none);
       in XML.Elem (markup, encode_thm thm_id thm) end;
 
     val _ = export_body thy "thms" (map export_thm (Global_Theory.dest_thm_names thy));
 
 
     (* type classes *)
 
     val encode_class =
       let open XML.Encode Term_XML.Encode
       in pair (list (pair string typ)) (list (encode_axiom Name.context)) end;
 
     fun export_class name =
       (case try (Axclass.get_info thy) name of
         NONE => ([], [])
       | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms))
       |> encode_class |> SOME;
 
     val _ =
       export_entities "classes" (fn name => fn () => export_class name)
         Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
 
 
     (* sort algebra *)
 
     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);
 
 
     (* locales *)
 
     fun encode_locale used =
       let open XML.Encode Term_XML.Encode in
         triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax))
           (list (encode_axiom used))
       end;
 
     fun export_locale loc =
       let
         val {typargs, args, axioms} = locale_content thy loc;
         val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context;
       in encode_locale used (typargs, args, axioms) end
       handle ERROR msg =>
         cat_error msg ("The error(s) above occurred in locale " ^
           quote (Locale.markup_name thy_ctxt loc));
 
     val _ =
       export_entities "locales" (fn loc => fn () => SOME (export_locale loc))
         Locale.locale_space (get_locales thy);
 
 
     (* locale dependencies *)
 
     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 consts)));
         in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
 
     val _ =
       get_dependencies parents thy
       |> map_index (fn (i, dep) =>
         let
           val xname = string_of_int (i + 1);
           val name = Long_Name.implode [Context.theory_name thy, xname];
           val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
           val body = encode_locale_dependency dep;
         in XML.Elem (markup, body) end)
       |> export_body thy "locale_dependencies";
 
 
     (* constdefs *)
 
     val constdefs =
       Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy)
       |> sort_by #1;
 
     val encode_constdefs =
       let open XML.Encode
       in list (pair string string) end;
 
     val _ =
       if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs);
 
 
     (* parents *)
 
     val _ =
       Export.export thy \<^path_binding>\<open>theory/parents\<close>
         (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
 
   in () end);
 
 end;