src/Pure/type_infer.ML

       let
         val (Ts_bTs', ts') = finish ctxt tye (Ts @ map snd bs, ts);
         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.mark_boundT xs, t) end;
+          in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
       in (map prep ts', Ts') end;
 
     fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
 
     fun unif_failed msg =