# HG changeset patch # User wenzelm # Date 1581870250 -3600 # Node ID 439410bf451928740a5a9f39a9a7222319b86b33 # Parent 91340a6bf401b12424fe22bf180b8eb8aec1ecb4 proper sort constraints for strip_shyps, which implicitly performs type instantiation; include solve_constraints in strip_shyps to avoid later conflicts with Thm.transfer; diff -r 91340a6bf401 -r 439410bf4519 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Feb 15 21:15:03 2020 +0100 +++ b/src/Pure/thm.ML Sun Feb 16 17:24:10 2020 +0100 @@ -1694,8 +1694,8 @@ end |> solve_constraints; (*Remove extra sorts that are witnessed by type signature information*) -fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm - | strip_shyps (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = +fun strip_shyps0 (thm as Thm (_, {shyps = [], ...})) = thm + | strip_shyps0 (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = let val thy = theory_of_thm thm; val algebra = Sign.classes_of thy; @@ -1705,14 +1705,18 @@ val witnessed = Sign.witness_sorts thy present extra; val extra' = fold (Sorts.remove_sort o #2) witnessed extra |> Sorts.minimal_sorts algebra; + val constraints' = fold (insert_constraints thy) witnessed 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, + {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; + + (*Internalize sort constraints of type variables*) val unconstrainT = solve_constraints #> (fn thm as Thm (der, args) =>