more robust and convenient treatment of implicit context;

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