more robust and convenient treatment of implicit context;
authorwenzelm
Wed, 07 Aug 2019 15:48:52 +0200
changeset 70668 d4b5139eea34
parent 70667 d9ba9563b139
child 70669 59250a328113
more robust and convenient treatment of implicit context;
src/Pure/thm.ML
--- 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