src/Pure/thm.ML
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