src/Pure/Thy/thy_output.ML
changeset 36446 06081e4921d6
parent 36323 655e2d74de3a
child 36745 403585a89772
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Apr 27 22:23:12 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Apr 28 08:25:02 2010 +0200
     1.3 @@ -453,7 +453,7 @@
     1.4  
     1.5  fun pretty_term_typ ctxt (style, t) =
     1.6    let val t' = style t
     1.7 -  in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t) end;
     1.8 +  in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t') t') end;
     1.9  
    1.10  fun pretty_term_typeof ctxt (style, t) =
    1.11    Syntax.pretty_typ ctxt (Term.fastype_of (style t));