# HG changeset patch
# User wenzelm
# Date 1530274792 -7200
# Node ID 6740e3611a869cebaac5d98d2915ea5122e9c632
# Parent  0903c4c8b4556aa6d38d29e36fbb8ef8d6203e96
disallow hyps in export;
handle extra shyps as explicit sort constraints;

diff -r 0903c4c8b455 -r 6740e3611a86 src/Pure/Thy/export_theory.ML
--- 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
diff -r 0903c4c8b455 -r 6740e3611a86 src/Pure/drule.ML
--- 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;