src/Pure/Thy/export_theory.ML
changeset 68727 ec0b2833cfc4
parent 68726 782d6b89fb19
child 68830 44ec6fdaacf8
equal deleted inserted replaced
68726:782d6b89fb19 68727:ec0b2833cfc4
   125         (#constants (Consts.dest (Sign.consts_of thy)));
   125         (#constants (Consts.dest (Sign.consts_of thy)));
   126 
   126 
   127 
   127 
   128     (* axioms and facts *)
   128     (* axioms and facts *)
   129 
   129 
   130     val standard_prop_of =
   130     fun standard_prop_of raw_thm =
   131       Thm.transfer thy #>
   131       let
   132       Thm.check_hyps (Context.Theory thy) #>
   132         val thm = raw_thm
   133       Drule.sort_constraint_intr_shyps #>
   133           |> Thm.transfer thy
   134       Thm.full_prop_of #>
   134           |> Thm.check_hyps (Context.Theory thy)
   135       Term_Subst.zero_var_indexes;
   135           |> Thm.strip_shyps;
   136 
   136         val prop = thm
   137     fun encode_prop prop =
   137           |> Thm.full_prop_of
       
   138           |> Term_Subst.zero_var_indexes;
       
   139       in (Thm.extra_shyps thm, prop) end;
       
   140 
       
   141     fun encode_prop (Ss, prop) =
   138       let
   142       let
   139         val prop' = Logic.unvarify_global (named_bounds prop);
   143         val prop' = Logic.unvarify_global (named_bounds prop);
   140         val typargs = rev (Term.add_tfrees prop' []);
   144         val typargs = rev (Term.add_tfrees prop' []);
       
   145         val sorts = Name.invent (Name.make_context (map #1 typargs)) Name.aT (length Ss) ~~ Ss;
   141         val args = rev (Term.add_frees prop' []);
   146         val args = rev (Term.add_frees prop' []);
   142         open XML.Encode Term_XML.Encode;
       
   143       in
   147       in
   144         triple (list (pair string sort)) (list (pair string typ)) term
   148         (sorts @ typargs, args, prop') |>
   145           (typargs, args, prop')
   149           let open XML.Encode Term_XML.Encode
       
   150           in triple (list (pair string sort)) (list (pair string typ)) term end
   146       end;
   151       end;
   147 
   152 
   148     val encode_fact = XML.Encode.list encode_prop o map standard_prop_of;
   153     val encode_fact = XML.Encode.list encode_prop o map standard_prop_of;
   149 
   154 
   150     val _ =
   155     val _ =
   151       export_entities "axioms" (K (SOME o encode_prop)) Theory.axiom_space
   156       export_entities "axioms" (fn _ => fn t => SOME (encode_prop ([], t))) Theory.axiom_space
   152         (Theory.axioms_of thy);
   157         (Theory.axioms_of thy);
   153     val _ =
   158     val _ =
   154       export_entities "facts" (K (SOME o encode_fact)) (Facts.space_of o Global_Theory.facts_of)
   159       export_entities "facts" (K (SOME o encode_fact)) (Facts.space_of o Global_Theory.facts_of)
   155         (Facts.dest_static true [] (Global_Theory.facts_of thy));
   160         (Facts.dest_static true [] (Global_Theory.facts_of thy));
   156 
   161