src/Pure/Thy/export_theory.ML
changeset 68206 dedf1a70d1fa
parent 68201 dee993b88a7b
child 68208 d9f2cf4fc002
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu May 17 16:42:13 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Thu May 17 17:29:17 2018 +0200
     1.3 @@ -27,6 +27,15 @@
     1.4  
     1.5  val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
     1.6    let
     1.7 +    (* parents *)
     1.8 +
     1.9 +    val parents = Theory.parents_of thy;
    1.10 +    val _ =
    1.11 +      export_body thy "parents"
    1.12 +        let open XML.Encode
    1.13 +        in list string (map Context.theory_long_name parents) end;
    1.14 +
    1.15 +
    1.16      (* entities *)
    1.17  
    1.18      fun entity_markup space name =
    1.19 @@ -40,7 +49,7 @@
    1.20      fun export_entities export_name export get_space decls =
    1.21        let val elems =
    1.22          let
    1.23 -          val parent_spaces = map get_space (Theory.parents_of thy);
    1.24 +          val parent_spaces = map get_space parents;
    1.25            val space = get_space thy;
    1.26          in
    1.27            (decls, []) |-> fold (fn (name, decl) =>