# HG changeset patch # User wenzelm # Date 1533546403 -7200 # Node ID ec0b2833cfc40e127ab34ca4f1fdb33fe80056c6 # Parent 782d6b89fb19cb6f74684a56dfaf38c52d91dca4 export shyps as regular typargs; diff -r 782d6b89fb19 -r ec0b2833cfc4 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sun Aug 05 20:32:18 2018 +0200 +++ b/src/Pure/Thy/export_theory.ML Mon Aug 06 11:06:43 2018 +0200 @@ -127,28 +127,33 @@ (* axioms and facts *) - val standard_prop_of = - Thm.transfer thy #> - Thm.check_hyps (Context.Theory thy) #> - Drule.sort_constraint_intr_shyps #> - Thm.full_prop_of #> - Term_Subst.zero_var_indexes; + fun standard_prop_of raw_thm = + let + val thm = raw_thm + |> Thm.transfer thy + |> Thm.check_hyps (Context.Theory thy) + |> Thm.strip_shyps; + val prop = thm + |> Thm.full_prop_of + |> Term_Subst.zero_var_indexes; + in (Thm.extra_shyps thm, prop) end; - fun encode_prop prop = + fun encode_prop (Ss, prop) = let val prop' = Logic.unvarify_global (named_bounds prop); val typargs = rev (Term.add_tfrees prop' []); + val sorts = Name.invent (Name.make_context (map #1 typargs)) Name.aT (length Ss) ~~ Ss; val args = rev (Term.add_frees prop' []); - open XML.Encode Term_XML.Encode; in - triple (list (pair string sort)) (list (pair string typ)) term - (typargs, args, prop') + (sorts @ typargs, args, prop') |> + let open XML.Encode Term_XML.Encode + in triple (list (pair string sort)) (list (pair string typ)) term end end; val encode_fact = XML.Encode.list encode_prop o map standard_prop_of; val _ = - export_entities "axioms" (K (SOME o encode_prop)) Theory.axiom_space + export_entities "axioms" (fn _ => fn t => SOME (encode_prop ([], t))) Theory.axiom_space (Theory.axioms_of thy); val _ = export_entities "facts" (K (SOME o encode_fact)) (Facts.space_of o Global_Theory.facts_of) diff -r 782d6b89fb19 -r ec0b2833cfc4 src/Pure/drule.ML --- a/src/Pure/drule.ML Sun Aug 05 20:32:18 2018 +0200 +++ b/src/Pure/drule.ML Mon Aug 06 11:06:43 2018 +0200 @@ -98,8 +98,6 @@ val is_sort_constraint: term -> bool val sort_constraintI: thm val sort_constraint_eq: thm - val sort_constraint_intr: indexname * sort -> thm -> thm - val sort_constraint_intr_shyps: thm -> thm val with_subgoal: int -> (thm -> thm) -> thm -> thm val comp_no_flatten: thm * int -> int -> thm -> thm val rename_bvars: (string * string) list -> thm -> thm @@ -649,26 +647,6 @@ (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI))) (implies_intr_list [A, C] (Thm.assume A))); -val sort_constraint_eq' = Thm.symmetric sort_constraint_eq; - -fun sort_constraint_intr tvar thm = - Thm.equal_elim - (Thm.instantiate - ([((("'a", 0), []), Thm.global_ctyp_of (Thm.theory_of_thm thm) (TVar tvar))], - [((("A", 0), propT), Thm.cprop_of thm)]) - sort_constraint_eq') thm; - -fun sort_constraint_intr_shyps raw_thm = - let val thm = Thm.strip_shyps raw_thm in - (case Thm.extra_shyps thm of - [] => thm - | shyps => - let - val names = Name.make_context (map #1 (Thm.fold_terms Term.add_tvar_names thm [])); - val constraints = map (rpair 0) (Name.invent names Name.aT (length shyps)) ~~ shyps; - in Thm.strip_shyps (fold_rev sort_constraint_intr constraints thm) end) - end; - end;