src/Pure/Thy/thy_output.ML
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));