src/Pure/Thy/export_theory.ML
changeset 68726 782d6b89fb19
parent 68725 367e60d9aa1b
child 68727 ec0b2833cfc4
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun Aug 05 14:50:11 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun Aug 05 20:32:18 2018 +0200
     1.3 @@ -131,27 +131,27 @@
     1.4        Thm.transfer thy #>
     1.5        Thm.check_hyps (Context.Theory thy) #>
     1.6        Drule.sort_constraint_intr_shyps #>
     1.7 -      Thm.full_prop_of;
     1.8 +      Thm.full_prop_of #>
     1.9 +      Term_Subst.zero_var_indexes;
    1.10  
    1.11 -    val encode_props =
    1.12 -      let open XML.Encode Term_XML.Encode
    1.13 -      in triple (list (pair string sort)) (list (pair string typ)) (list (term o named_bounds)) end;
    1.14 -
    1.15 -    fun export_props props =
    1.16 +    fun encode_prop prop =
    1.17        let
    1.18 -        val props' = map Logic.unvarify_global props;
    1.19 -        val typargs = rev (fold Term.add_tfrees props' []);
    1.20 -        val args = rev (fold Term.add_frees props' []);
    1.21 -      in encode_props (typargs, args, props') end;
    1.22 +        val prop' = Logic.unvarify_global (named_bounds prop);
    1.23 +        val typargs = rev (Term.add_tfrees prop' []);
    1.24 +        val args = rev (Term.add_frees prop' []);
    1.25 +        open XML.Encode Term_XML.Encode;
    1.26 +      in
    1.27 +        triple (list (pair string sort)) (list (pair string typ)) term
    1.28 +          (typargs, args, prop')
    1.29 +      end;
    1.30  
    1.31 -    val export_axiom = export_props o single;
    1.32 -    val export_fact = export_props o Term_Subst.zero_var_indexes_list o map standard_prop_of;
    1.33 +    val encode_fact = XML.Encode.list encode_prop o map standard_prop_of;
    1.34  
    1.35      val _ =
    1.36 -      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
    1.37 +      export_entities "axioms" (K (SOME o encode_prop)) Theory.axiom_space
    1.38          (Theory.axioms_of thy);
    1.39      val _ =
    1.40 -      export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of)
    1.41 +      export_entities "facts" (K (SOME o encode_fact)) (Facts.space_of o Global_Theory.facts_of)
    1.42          (Facts.dest_static true [] (Global_Theory.facts_of thy));
    1.43  
    1.44