diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/code.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -110,7 +110,8 @@
 
 (* printing *)
 
-fun string_of_typ thy = setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy);
+fun string_of_typ thy =
+  Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));
 
 fun string_of_const thy c = case AxClass.inst_of_param thy c
  of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)