src/Pure/term.ML
changeset 60311 599c4a27785c
parent 56245 84fc7dfa3cd4
child 60404 422b63ef0147
equal deleted inserted replaced
60310:932221b62e89 60311:599c4a27785c
   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'*)