summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 16 Feb 2020 17:24:10 +0100 | |

changeset 71660 | 439410bf4519 |

parent 71658 | 91340a6bf401 |

child 71661 | 404624eb3a22 |

proper sort constraints for strip_shyps, which implicitly performs type instantiation;
include solve_constraints in strip_shyps to avoid later conflicts with Thm.transfer;

src/Pure/thm.ML | file | annotate | diff | comparison | revisions |

--- 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) =>