equal
deleted
inserted
replaced
287 | TVar v => raise TERM (funerr, [f $ u]) |
287 | TVar v => raise TERM (funerr, [f $ u]) |
288 | _ => raise TERM (funerr, [f $ u])) |
288 | _ => raise TERM (funerr, [f $ u])) |
289 | fast Ts (Const (_, T)) = T |
289 | fast Ts (Const (_, T)) = T |
290 | fast Ts (Free (_, T)) = T |
290 | fast Ts (Free (_, T)) = T |
291 | fast Ts (Bound i) = |
291 | fast Ts (Bound i) = |
292 (nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i])) |
292 (nth Ts i handle General.Subscript => raise TERM ("fastype: Bound", [Bound i])) |
293 | fast Ts (Var (_, T)) = T |
293 | fast Ts (Var (_, T)) = T |
294 | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u; |
294 | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u; |
295 in fast end; |
295 in fast end; |
296 |
296 |
297 |
297 |