# HG changeset patch
# User wenzelm
# Date 1565185732 -7200
# Node ID d4b5139eea34a135695282e2228db34f3c1fee35
# Parent  d9ba9563b139663cb84e1eb2a12837b281b4293f
more robust and convenient treatment of implicit context;

diff -r d9ba9563b139 -r d4b5139eea34 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