src/Pure/Thy/export_theory.ML
changeset 68295 781a98696638
parent 68264 bb9a3be6952a
child 68539 6740e3611a86
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sat May 26 21:24:07 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sat May 26 22:02:25 2018 +0200
     1.3 @@ -141,6 +141,24 @@
     1.4        export_entities "classes" (fn name => fn () => export_class name)
     1.5          Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
     1.6  
     1.7 -    in () end);
     1.8 +
     1.9 +    (* sort algebra *)
    1.10 +
    1.11 +    val {classrel, arities} =
    1.12 +      Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
    1.13 +        (#2 (#classes rep_tsig));
    1.14 +
    1.15 +    val encode_classrel =
    1.16 +      let open XML.Encode
    1.17 +      in list (pair string (list string)) end;
    1.18 +
    1.19 +    val encode_arities =
    1.20 +      let open XML.Encode Term_XML.Encode
    1.21 +      in list (triple string (list sort) string) end;
    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 +
    1.26 +  in () end);
    1.27  
    1.28  end;