src/Tools/Code/code_thingol.ML

--- a/src/Tools/Code/code_thingol.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -412,7 +412,7 @@
 
 fun not_wellsorted ctxt permissive some_thm deps ty sort e =
   let
-    val err_class = Sorts.class_error (Context.pretty ctxt) e;
+    val err_class = Sorts.class_error (Context.Proof ctxt) e;
     val err_typ =
       "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
         Syntax.string_of_sort ctxt sort;