src/Pure/type_infer_context.ML
changeset 49660 de49d9b4d7bc
parent 47291 6a641856a0e9
child 56438 7f6b2634d853
     1.1 --- a/src/Pure/type_infer_context.ML	Sat Sep 29 16:51:04 2012 +0200
     1.2 +++ b/src/Pure/type_infer_context.ML	Sat Sep 29 18:23:46 2012 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4          val (Ts', Ts'') = chop (length Ts) Ts_bTs';
     1.5          fun prep t =
     1.6            let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
     1.7 -          in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
     1.8 +          in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
     1.9        in (map prep ts', Ts') end;
    1.10  
    1.11      fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);