# 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*)