src/ZF/Resid/Redex.thy

--- a/src/ZF/Resid/Redex.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Redex.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -22,7 +22,7 @@
 defs
   redex_rec_def
    "redex_rec(p,b,c,d) == 
-   Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),   
-                             %n x y.d(n, x, y, g`x, g`y), p))"
+   Vrec(p, %p g. redexes_case(b, %x. c(x,g`x),   
+                             %n x y. d(n, x, y, g`x, g`y), p))"
 end