diff -r 70d3915c92f0 -r 917b4b6ba3d2 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Sep 05 21:41:24 2010 +0200
@@ -215,7 +215,7 @@
     val thy = ProofContext.theory_of ctxt;
     val certT = Thm.ctyp_of thy;
     val cert = Thm.cterm_of thy;
-    val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term ctxt);
+    val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
 
     fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);