src/Pure/goal_display.ML
changeset 52284 b12f2cef3ee5
parent 52211 66bc827e37f8
child 56438 7f6b2634d853
     1.1 --- a/src/Pure/goal_display.ML	Sat Jun 01 12:03:37 2013 +0200
     1.2 +++ b/src/Pure/goal_display.ML	Sat Jun 01 14:16:10 2013 +0200
     1.3 @@ -81,7 +81,10 @@
     1.4  
     1.5      val prt_sort = Syntax.pretty_sort ctxt;
     1.6      val prt_typ = Syntax.pretty_typ ctxt;
     1.7 -    val prt_term = Syntax.pretty_term ctxt o Type_Annotation.ignore_free_types;
     1.8 +    val prt_term =
     1.9 +      singleton (Syntax.uncheck_terms ctxt) #>
    1.10 +      Type_Annotation.ignore_free_types #>
    1.11 +      Syntax.unparse_term ctxt;
    1.12  
    1.13      fun prt_atoms prt prtT (X, xs) = Pretty.block
    1.14        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",