diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -582,7 +582,7 @@
 
 fun not_wellsorted thy permissive some_thm ty sort e =
   let
-    val err_class = Sorts.class_error (Syntax.pp_global thy) e;
+    val err_class = Sorts.class_error (Context.pretty_global thy) e;
     val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
       ^ Syntax.string_of_sort_global thy sort;
   in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;