src/Pure/Thy/thy_output.ML
changeset 39288 f1ae2493d93f
parent 39134 917b4b6ba3d2
child 39308 c2c9bb3c52c6
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sun Sep 12 17:39:02 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Sep 12 19:04:02 2010 +0200
     1.3 @@ -482,7 +482,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 (Type_Infer.constrain (Term.fastype_of t') t') end;
     1.8 +  in pretty_term ctxt (Type.constraint (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));