# HG changeset patch
# User wenzelm
# Date 1703934763 -3600
# Node ID 25fa3bc05a5152f536f0357e66b91038bbeda8ed
# Parent  bd52ab785b7b8ffff6dcc8df69d7a95267087893
clarified modules;
minor performance tuning;

diff -r bd52ab785b7b -r 25fa3bc05a51 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Dec 30 11:26:05 2023 +0100
+++ b/src/Pure/proofterm.ML	Sat Dec 30 12:12:43 2023 +0100
@@ -145,8 +145,6 @@
   val abstract_rule_proof: string * term -> proof -> proof
   val combination_proof: term -> term -> term -> term -> proof -> proof -> proof
   val could_unify: proof * proof -> bool
-  val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
-    sort list -> proof -> proof
   val of_sort_proof: Sorts.algebra ->
     (class * class -> proof) ->
     (string * class list list * class -> proof) ->
@@ -1100,20 +1098,6 @@
 
 (** type classes **)
 
-fun strip_shyps_proof algebra present witnessed extra prf =
-  let
-    val replacements = present @ witnessed @ map (`Logic.dummy_tfree) extra;
-    fun get_replacement S =
-      replacements |> get_first (fn (T', S') =>
-        if Sorts.sort_le algebra (S', S) then SOME T' else NONE);
-    fun replace T =
-      if exists (fn (T', _) => T' = T) present then raise Same.SAME
-      else
-        (case get_replacement (Type.sort_of_atyp T) of
-          SOME T' => T'
-        | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term");
-  in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
-
 fun of_sort_proof algebra classrel_proof arity_proof hyps =
   Sorts.of_sort_derivation algebra
    {class_relation = fn _ => fn _ => fn (prf, c1) => fn c2 =>
diff -r bd52ab785b7b -r 25fa3bc05a51 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 30 11:26:05 2023 +0100
+++ b/src/Pure/thm.ML	Sat Dec 30 12:12:43 2023 +0100
@@ -1055,6 +1055,8 @@
     Thm (_, {shyps = [], ...}) => thm
   | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) =>
       let
+        val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
+
         val thy = theory_of_thm thm;
 
         val algebra = Sign.classes_of thy;
@@ -1084,8 +1086,18 @@
         val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints;
         val shyps' = fold (Sorts.insert_sort o #2) present extra';
 
-        val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
-        val proof' = Proofterm.strip_shyps_proof algebra present witnessed extra' proof;
+        val replacements = present @ witnessed @ map (`Logic.dummy_tfree) extra';
+        fun get_replacement S =
+          replacements |> get_first (fn (T', S') => if le (S', S) then SOME T' else NONE);
+        fun replace_atyp T =
+          if Types.defined present_set T then raise Same.SAME
+          else
+            (case get_replacement (Type.sort_of_atyp T) of
+              SOME T' => T'
+            | NONE => raise Fail "strip_shyps: bad type variable in proof term");
+
+        val proof' = proof
+          |> Same.commit (Proofterm.map_proof_types_same (Term_Subst.map_atypsT_same replace_atyp));
       in
         Thm (make_deriv promises oracles thms zboxes zproof proof',
          {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',