src/Pure/envir.ML
changeset 43278 1fbdcebb364b
parent 42083 e1209fc7ecdc
child 51700 c8f2bad67dbb
equal deleted inserted replaced
43277:1fd31f859fc7 43278:1fbdcebb364b
   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