changeset 70482 | d4b5139eea34 |
parent 70480 | 1a1b7d7f24bb |
child 70494 | 41108e3e9ca5 |
--- a/src/Pure/thm.ML Wed Aug 07 11:09:37 2019 +0200 +++ b/src/Pure/thm.ML Wed Aug 07 15:48:52 2019 +0200 @@ -1650,7 +1650,7 @@ tpairs = [], prop = prop}) else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, []) - end; + end |> solve_constraints; (*Remove extra sorts that are witnessed by type signature information*) fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm