src/ZF/Resid/Terms.thy

--- a/src/ZF/Resid/Terms.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Terms.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -24,9 +24,9 @@
   type_intrs	"redexes.intrs@bool_typechecks"
 
 defs
-  unmark_def	"unmark(u) == redex_rec(u,%i.Var(i),   \
-\		                          %x m.Fun(m),   \
-\		                          %b x y m p.Apl(m,p))"
+  unmark_def	"unmark(u) == redex_rec(u,%i.Var(i),   
+		                          %x m.Fun(m),   
+		                          %b x y m p.Apl(m,p))"
 end