Type_Annotation only works *after* uncheck (which usually requires authentic type information);

--- a/src/Pure/goal_display.ML	Sat Jun 01 12:03:37 2013 +0200
+++ b/src/Pure/goal_display.ML	Sat Jun 01 14:16:10 2013 +0200
@@ -81,7 +81,10 @@
 
     val prt_sort = Syntax.pretty_sort ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
-    val prt_term = Syntax.pretty_term ctxt o Type_Annotation.ignore_free_types;
+    val prt_term =
+      singleton (Syntax.uncheck_terms ctxt) #>
+      Type_Annotation.ignore_free_types #>
+      Syntax.unparse_term ctxt;
 
     fun prt_atoms prt prtT (X, xs) = Pretty.block
       [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",