--- a/src/Pure/Syntax/syntax.ML Sun Sep 05 22:23:48 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Sun Sep 05 23:16:21 2010 +0200
@@ -760,7 +760,7 @@
val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
val len = length results;
- val show_term = setmp_CRITICAL Printer.show_brackets true (string_of_term ctxt);
+ val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
in
if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
else if len = 1 then