changeset 39288 | f1ae2493d93f |
parent 39134 | 917b4b6ba3d2 |
child 39308 | c2c9bb3c52c6 |
--- a/src/Pure/Thy/thy_output.ML Sun Sep 12 17:39:02 2010 +0200 +++ b/src/Pure/Thy/thy_output.ML Sun Sep 12 19:04:02 2010 +0200 @@ -482,7 +482,7 @@ fun pretty_term_typ ctxt (style, t) = let val t' = style t - in pretty_term ctxt (Type_Infer.constrain (Term.fastype_of t') t') end; + in pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end; fun pretty_term_typeof ctxt (style, t) = Syntax.pretty_typ ctxt (Term.fastype_of (style t));