# HG changeset patch
# User wenzelm
# Date 1583755422 -3600
# Node ID 4d412964a61acf29539c0f3c3bc1f60deea7178f
# Parent  abe723ff3f7fe1ea9ba43795bb354a821e3d3b24
tuned signature;

diff -r abe723ff3f7f -r 4d412964a61a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Mar 09 11:52:28 2020 +0100
+++ b/src/Pure/thm.ML	Mon Mar 09 13:03:42 2020 +0100
@@ -97,7 +97,6 @@
   val renamed_prop: term -> thm -> thm
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
-  val extra_shyps: thm -> sort list
   val proof_bodies_of: thm list -> proof_body list
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
@@ -107,6 +106,8 @@
   val expose_proof: theory -> thm -> unit
   val future: thm future -> cterm -> thm
   val thm_deps: thm -> Proofterm.thm Ord_List.T
+  val extra_shyps: thm -> sort list
+  val strip_shyps: thm -> thm
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
   val derivation_id: thm -> Proofterm.thm_id option
@@ -159,7 +160,6 @@
     cterm -> cterm
   val trivial: cterm -> thm
   val of_class: ctyp * class -> thm
-  val strip_shyps: thm -> thm
   val unconstrainT: thm -> thm
   val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val varifyT_global: thm -> thm
@@ -699,10 +699,6 @@
     val sorts' = Sorts.union sorts more_sorts;
   in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
 
-(*dangling sort constraints of a thm*)
-fun extra_shyps (th as Thm (_, {shyps, ...})) =
-  Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
-
 
 
 (** derivations and promised proofs **)
@@ -988,6 +984,49 @@
 
 end;
 
+(*Dangling sort constraints of a thm*)
+fun extra_shyps (th as Thm (_, {shyps, ...})) =
+  Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
+
+(*Remove extra sorts that are witnessed by type signature information*)
+fun strip_shyps thm =
+  (case thm of
+    Thm (_, {shyps = [], ...}) => thm
+  | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) =>
+      let
+        val thy = theory_of_thm thm;
+
+        val algebra = Sign.classes_of thy;
+        val minimize = Sorts.minimize_sort algebra;
+        val le = Sorts.sort_le algebra;
+        fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1));
+        fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];
+
+        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
+        val extra = fold (Sorts.remove_sort o #2) present shyps;
+        val witnessed = Sign.witness_sorts thy present extra;
+        val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize);
+
+        val extra' =
+          non_witnessed |> map_filter (fn (S, _) =>
+            if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S)
+          |> Sorts.make;
+
+        val constrs' =
+          non_witnessed |> maps (fn (S1, S2) =>
+            let val S0 = the (find_first (fn S => le (S, S1)) extra')
+            in rel (S0, S1) @ rel (S1, S2) end);
+
+        val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints;
+        val shyps' = fold (Sorts.insert_sort o #2) present extra';
+      in
+        Thm (deriv_rule_unconditional
+          (Proofterm.strip_shyps_proof algebra present witnessed extra') der,
+         {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
+          shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
+      end)
+  |> solve_constraints;
+
 
 
 (*** Closed theorems with official name ***)
@@ -1693,46 +1732,6 @@
     else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
   end |> solve_constraints;
 
-(*Remove extra sorts that are witnessed by type signature information*)
-fun strip_shyps thm =
-  (case thm of
-    Thm (_, {shyps = [], ...}) => thm
-  | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) =>
-      let
-        val thy = theory_of_thm thm;
-
-        val algebra = Sign.classes_of thy;
-        val minimize = Sorts.minimize_sort algebra;
-        val le = Sorts.sort_le algebra;
-        fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1));
-        fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];
-
-        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
-        val extra = fold (Sorts.remove_sort o #2) present shyps;
-        val witnessed = Sign.witness_sorts thy present extra;
-        val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize);
-
-        val extra' =
-          non_witnessed |> map_filter (fn (S, _) =>
-            if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S)
-          |> Sorts.make;
-
-        val constrs' =
-          non_witnessed |> maps (fn (S1, S2) =>
-            let val S0 = the (find_first (fn S => le (S, S1)) extra')
-            in rel (S0, S1) @ rel (S1, S2) end);
-
-        val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints;
-        val shyps' = fold (Sorts.insert_sort o #2) present extra';
-      in
-        Thm (deriv_rule_unconditional
-          (Proofterm.strip_shyps_proof algebra present witnessed extra') der,
-         {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
-          shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
-      end)
-  |> solve_constraints;
-
-
 (*Internalize sort constraints of type variables*)
 val unconstrainT =
   solve_constraints #> (fn thm as Thm (der, args) =>