src/Tools/subtyping.ML

--- a/src/Tools/subtyping.ML	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/Tools/subtyping.ML	Sat Sep 29 18:23:46 2012 +0200
@@ -231,7 +231,7 @@
     val (Ts', Ts'') = chop (length Ts) Ts_bTs';
     fun prep t =
       let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
-      in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
+      in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
   in (map prep ts', Ts') end;
 
 fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);