577 val a_itselfT = itselfT (TFree (Name.aT, [])); |
577 val a_itselfT = itselfT (TFree (Name.aT, [])); |
578 |
578 |
579 val propT : typ = Type ("prop",[]); |
579 val propT : typ = Type ("prop",[]); |
580 |
580 |
581 (* maps !!x1...xn. t to t *) |
581 (* maps !!x1...xn. t to t *) |
582 fun strip_all_body (Const("Pure.all",_)$Abs(_,_,t)) = strip_all_body t |
582 fun strip_all_body (Const ("Pure.all", _) $ Abs (_, _, t)) = strip_all_body t |
583 | strip_all_body t = t; |
583 | strip_all_body t = t; |
584 |
584 |
585 (* maps !!x1...xn. t to [x1, ..., xn] *) |
585 (* maps !!x1...xn. t to [x1, ..., xn] *) |
586 fun strip_all_vars (Const("Pure.all",_)$Abs(a,T,t)) = |
586 fun strip_all_vars (Const ("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t |
587 (a,T) :: strip_all_vars t |
587 | strip_all_vars t = []; |
588 | strip_all_vars t = [] : (string*typ) list; |
|
589 |
588 |
590 (*increments a term's non-local bound variables |
589 (*increments a term's non-local bound variables |
591 required when moving a term within abstractions |
590 required when moving a term within abstractions |
592 inc is increment for bound variables |
591 inc is increment for bound variables |
593 lev is level at which a bound variable is considered 'loose'*) |
592 lev is level at which a bound variable is considered 'loose'*) |