# 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;