src/Pure/Thy/export_theory.ML
changeset 68539 6740e3611a86
parent 68295 781a98696638
child 68724 7fafadbf16c7
     1.1 --- a/src/Pure/Thy/export_theory.ML	Fri Jun 29 14:02:14 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Fri Jun 29 14:19:52 2018 +0200
     1.3 @@ -102,6 +102,12 @@
     1.4  
     1.5      (* axioms and facts *)
     1.6  
     1.7 +    val standard_prop_of =
     1.8 +      Thm.transfer thy #>
     1.9 +      Thm.check_hyps (Context.Theory thy) #>
    1.10 +      Drule.sort_constraint_intr_shyps #>
    1.11 +      Thm.full_prop_of;
    1.12 +
    1.13      val encode_props =
    1.14        let open XML.Encode Term_XML.Encode
    1.15        in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
    1.16 @@ -114,7 +120,7 @@
    1.17        in encode_props (typargs, args, props') end;
    1.18  
    1.19      val export_axiom = export_props o single;
    1.20 -    val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of;
    1.21 +    val export_fact = export_props o Term_Subst.zero_var_indexes_list o map standard_prop_of;
    1.22  
    1.23      val _ =
    1.24        export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space