src/Pure/Thy/export_theory.ML
changeset 68727 ec0b2833cfc4
parent 68726 782d6b89fb19
child 68830 44ec6fdaacf8
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun Aug 05 20:32:18 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Mon Aug 06 11:06:43 2018 +0200
     1.3 @@ -127,28 +127,33 @@
     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 -      Term_Subst.zero_var_indexes;
    1.13 +    fun standard_prop_of raw_thm =
    1.14 +      let
    1.15 +        val thm = raw_thm
    1.16 +          |> Thm.transfer thy
    1.17 +          |> Thm.check_hyps (Context.Theory thy)
    1.18 +          |> Thm.strip_shyps;
    1.19 +        val prop = thm
    1.20 +          |> Thm.full_prop_of
    1.21 +          |> Term_Subst.zero_var_indexes;
    1.22 +      in (Thm.extra_shyps thm, prop) end;
    1.23  
    1.24 -    fun encode_prop prop =
    1.25 +    fun encode_prop (Ss, prop) =
    1.26        let
    1.27          val prop' = Logic.unvarify_global (named_bounds prop);
    1.28          val typargs = rev (Term.add_tfrees prop' []);
    1.29 +        val sorts = Name.invent (Name.make_context (map #1 typargs)) Name.aT (length Ss) ~~ Ss;
    1.30          val args = rev (Term.add_frees prop' []);
    1.31 -        open XML.Encode Term_XML.Encode;
    1.32        in
    1.33 -        triple (list (pair string sort)) (list (pair string typ)) term
    1.34 -          (typargs, args, prop')
    1.35 +        (sorts @ typargs, args, prop') |>
    1.36 +          let open XML.Encode Term_XML.Encode
    1.37 +          in triple (list (pair string sort)) (list (pair string typ)) term end
    1.38        end;
    1.39  
    1.40      val encode_fact = XML.Encode.list encode_prop o map standard_prop_of;
    1.41  
    1.42      val _ =
    1.43 -      export_entities "axioms" (K (SOME o encode_prop)) Theory.axiom_space
    1.44 +      export_entities "axioms" (fn _ => fn t => SOME (encode_prop ([], t))) Theory.axiom_space
    1.45          (Theory.axioms_of thy);
    1.46      val _ =
    1.47        export_entities "facts" (K (SOME o encode_fact)) (Facts.space_of o Global_Theory.facts_of)