diff -r c3913a79b6ae -r 492493334e0f ex/Term.thy
--- a/ex/Term.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/Term.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -40,12 +40,12 @@
 
   (*list recursion*)
   Term_rec_def	
-   "Term_rec(M,d) == wfrec(trancl(pred_sexp),  M, \
-\            Split(%x y g. d(x,y, Abs_map(g,y))))"
+   "Term_rec(M,d) == wfrec(trancl(pred_sexp),  M, 
+            Split(%x y g. d(x,y, Abs_map(g,y))))"
 
   term_rec_def
-   "term_rec(t,d) == \
-\   Term_rec(Rep_term(t), %x y r. d(Inv(Leaf,x), Abs_Tlist(y), r))"
+   "term_rec(t,d) == 
+   Term_rec(Rep_term(t), %x y r. d(Inv(Leaf,x), Abs_Tlist(y), r))"
 
 rules
     (*faking a type definition for term...*)