src/Pure/sign.ML
changeset 37145 01aa36932739
parent 36610 bafd82950e24
child 39133 70d3915c92f0
     1.1 --- a/src/Pure/sign.ML	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu May 27 17:41:27 2010 +0200
     1.3 @@ -271,7 +271,7 @@
     1.4          val t' = subst_bounds (xs, t);
     1.5          val u' = subst_bounds (xs, u);
     1.6          val msg = cat_lines
     1.7 -          (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
     1.8 +          (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
     1.9        in raise TYPE (msg, [T, U], [t', u']) end;
    1.10  
    1.11      fun typ_of (_, Const (_, T)) = T