src/ZF/Resid/Redex.thy

     Logic Image: ZF
 *)
 
 Redex = Univ +
 consts
-  redexes     :: "i"
+  redexes     :: i
 
 datatype
   "redexes" = Var ("n: nat")	        
             | Fun ("t: redexes")
             | App ("b:bool" ,"f:redexes" , "a:redexes")
   type_intrs "[bool_into_univ]"
   
 
 consts
-  redex_rec   	:: "[i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i"
+  redex_rec   	:: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
  
 defs
   redex_rec_def
    "redex_rec(p,b,c,d) == 
    Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),