src/Pure/Thy/export_theory.ML
changeset 70386 6af87375b95f
parent 70384 8ce08b154aa1
child 70529 2ecbbe6b35db
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sat Jul 20 14:03:51 2019 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun Jul 21 12:11:35 2019 +0200
     1.3 @@ -290,8 +290,9 @@
     1.4  
     1.5      fun encode_axiom used t = encode_prop used ([], t);
     1.6  
     1.7 -    val encode_fact_single = encode_prop Name.context o prop_of;
     1.8 -    val encode_fact_multi = XML.Encode.list (encode_prop Name.context) o map prop_of;
     1.9 +    val encode_fact = encode_prop Name.context;
    1.10 +    val encode_fact_single = encode_fact o prop_of;
    1.11 +    val encode_fact_multi = XML.Encode.list encode_fact o map prop_of;
    1.12  
    1.13      val _ =
    1.14        export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
    1.15 @@ -321,25 +322,27 @@
    1.16  
    1.17      (* sort algebra *)
    1.18  
    1.19 -    val {classrel, arities} =
    1.20 -      Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
    1.21 -        (#2 (#classes rep_tsig));
    1.22 +    local
    1.23 +      val prop = encode_axiom Name.context o Logic.varify_global;
    1.24  
    1.25 -    val encode_prop0 =
    1.26 -      encode_axiom Name.context o Logic.varify_global;
    1.27 +      val encode_classrel =
    1.28 +        let open XML.Encode
    1.29 +        in list (pair prop (pair string string)) end;
    1.30  
    1.31 -    val encode_classrel =
    1.32 -      let open XML.Encode
    1.33 -      in list (pair encode_prop0 (pair string string)) end;
    1.34 +      val encode_arities =
    1.35 +        let open XML.Encode Term_XML.Encode
    1.36 +        in list (pair prop (triple string (list sort) string)) end;
    1.37 +    in
    1.38 +      val export_classrel =
    1.39 +        maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel;
    1.40  
    1.41 -    val encode_arities =
    1.42 -      let open XML.Encode Term_XML.Encode
    1.43 -      in list (pair encode_prop0 (triple string (list sort) string)) end;
    1.44 +      val export_arities = map (`Logic.mk_arity) #> encode_arities;
    1.45  
    1.46 -    val export_classrel =
    1.47 -      maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel;
    1.48 +      val {classrel, arities} =
    1.49 +        Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
    1.50 +          (#2 (#classes rep_tsig));
    1.51  
    1.52 -    val export_arities = map (`Logic.mk_arity) #> encode_arities;
    1.53 +    end;
    1.54  
    1.55      val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel);
    1.56      val _ = if null arities then () else export_body thy "arities" (export_arities arities);