268 fun err_appl why bs t T u U = |
268 fun err_appl why bs t T u U = |
269 let |
269 let |
270 val xs = map Free bs; (*we do not rename here*) |
270 val xs = map Free bs; (*we do not rename here*) |
271 val t' = subst_bounds (xs, t); |
271 val t' = subst_bounds (xs, t); |
272 val u' = subst_bounds (xs, u); |
272 val u' = subst_bounds (xs, u); |
273 val msg = cat_lines |
273 val msg = cat_lines (Type_Infer.appl_error pp why t' T u' U); |
274 (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U); |
|
275 in raise TYPE (msg, [T, U], [t', u']) end; |
274 in raise TYPE (msg, [T, U], [t', u']) end; |
276 |
275 |
277 fun typ_of (_, Const (_, T)) = T |
276 fun typ_of (_, Const (_, T)) = T |
278 | typ_of (_, Free (_, T)) = T |
277 | typ_of (_, Free (_, T)) = T |
279 | typ_of (_, Var (_, T)) = T |
278 | typ_of (_, Var (_, T)) = T |