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