diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/ex/Term.thy
--- a/src/HOL/ex/Term.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/Term.thy	Wed Jun 21 15:47:10 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...*)