changeset 42284 | 326f57825e1a |
parent 42143 | 786ccfffcd67 |
child 42360 | da8817d01e7c |
--- a/src/Pure/type_infer.ML Fri Apr 08 11:39:45 2011 +0200 +++ b/src/Pure/type_infer.ML Fri Apr 08 13:31:16 2011 +0200 @@ -300,7 +300,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.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);