src/Pure/Thy/export_theory.ML
changeset 70384 8ce08b154aa1
parent 70015 c8e08d8ffb93
child 70386 6af87375b95f
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sat Jul 20 11:48:30 2019 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sat Jul 20 12:52:29 2019 +0200
     1.3 @@ -325,16 +325,24 @@
     1.4        Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
     1.5          (#2 (#classes rep_tsig));
     1.6  
     1.7 +    val encode_prop0 =
     1.8 +      encode_axiom Name.context o Logic.varify_global;
     1.9 +
    1.10      val encode_classrel =
    1.11        let open XML.Encode
    1.12 -      in list (pair string (list string)) end;
    1.13 +      in list (pair encode_prop0 (pair string string)) end;
    1.14  
    1.15      val encode_arities =
    1.16        let open XML.Encode Term_XML.Encode
    1.17 -      in list (triple string (list sort) string) end;
    1.18 +      in list (pair encode_prop0 (triple string (list sort) string)) end;
    1.19 +
    1.20 +    val export_classrel =
    1.21 +      maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel;
    1.22  
    1.23 -    val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel);
    1.24 -    val _ = if null arities then () else export_body thy "arities" (encode_arities arities);
    1.25 +    val export_arities = map (`Logic.mk_arity) #> encode_arities;
    1.26 +
    1.27 +    val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel);
    1.28 +    val _ = if null arities then () else export_body thy "arities" (export_arities arities);
    1.29  
    1.30  
    1.31      (* locales *)