src/Pure/type_infer.ML
changeset 42383 0ae4ad40d7b5
parent 42360 da8817d01e7c
child 42386 50ea65e84d98
--- a/src/Pure/type_infer.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/type_infer.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -289,7 +289,7 @@
 
 fun infer ctxt =
   let
-    val pp = Syntax.pp ctxt;
+    val pp = Context.pretty ctxt;
 
 
     (* errors *)
@@ -310,7 +310,7 @@
 
     fun err_appl msg tye bs t T u U =
       let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
-      in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
+      in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
 
 
     (* main *)