--- a/src/Pure/Thy/export_theory.ML Fri Jun 29 14:02:14 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML Fri Jun 29 14:19:52 2018 +0200
@@ -102,6 +102,12 @@
(* 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;
+
val encode_props =
let open XML.Encode Term_XML.Encode
in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
@@ -114,7 +120,7 @@
in encode_props (typargs, args, props') end;
val export_axiom = export_props o single;
- val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of;
+ val export_fact = export_props o Term_Subst.zero_var_indexes_list o map standard_prop_of;
val _ =
export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
--- a/src/Pure/drule.ML Fri Jun 29 14:02:14 2018 +0200
+++ b/src/Pure/drule.ML Fri Jun 29 14:19:52 2018 +0200
@@ -98,6 +98,8 @@
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
@@ -647,6 +649,26 @@
(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;