diff -r fd6308b4df72 -r 01aa36932739 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu May 27 17:41:27 2010 +0200
@@ -455,7 +455,7 @@
 
 fun pretty_term_typ ctxt (style, t) =
   let val t' = style t
-  in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t') t') end;
+  in pretty_term ctxt (Type_Infer.constrain (Term.fastype_of t') t') end;
 
 fun pretty_term_typeof ctxt (style, t) =
   Syntax.pretty_typ ctxt (Term.fastype_of (style t));