src/Pure/type_infer.ML
changeset 42383 0ae4ad40d7b5
parent 42360 da8817d01e7c
child 42386 50ea65e84d98
     1.1 --- a/src/Pure/type_infer.ML	Sun Apr 17 23:47:05 2011 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Mon Apr 18 11:13:29 2011 +0200
     1.3 @@ -289,7 +289,7 @@
     1.4  
     1.5  fun infer ctxt =
     1.6    let
     1.7 -    val pp = Syntax.pp ctxt;
     1.8 +    val pp = Context.pretty ctxt;
     1.9  
    1.10  
    1.11      (* errors *)
    1.12 @@ -310,7 +310,7 @@
    1.13  
    1.14      fun err_appl msg tye bs t T u U =
    1.15        let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
    1.16 -      in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
    1.17 +      in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
    1.18  
    1.19  
    1.20      (* main *)