# HG changeset patch
# User wenzelm
# Date 1581934629 -3600
# Node ID fb08117a106ba1a7a791983f705caccb9a51aea9
# Parent  efcd6742ea9c908b05ffa4d06ea973b7fe4c7caa
tuned;

diff -r efcd6742ea9c -r fb08117a106b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Feb 16 21:11:28 2020 +0100
+++ b/src/Pure/thm.ML	Mon Feb 17 11:17:09 2020 +0100
@@ -1694,8 +1694,10 @@
   end |> solve_constraints;
 
 (*Remove extra sorts that are witnessed by type signature information*)
-fun strip_shyps0 (thm as Thm (_, {shyps = [], ...})) = thm
-  | strip_shyps0 (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
+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;
@@ -1712,9 +1714,8 @@
           (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;
-
-val strip_shyps = solve_constraints #> strip_shyps0 #> solve_constraints;
+      end)
+  |> solve_constraints;
 
 
 (*Internalize sort constraints of type variables*)