diff -r 9a6e7bd2bfaf -r 9b3d3362a048 src/FOL/ex/List.thy
--- a/src/FOL/ex/List.thy	Tue Nov 07 12:57:20 1995 +0100
+++ b/src/FOL/ex/List.thy	Tue Nov 07 12:58:17 1995 +0100
@@ -12,14 +12,14 @@
 arities list :: (term)term
 
 consts
-   hd		:: "'a list => 'a"
-   tl		:: "'a list => 'a list"
-   forall	:: "['a list, 'a => o] => o"
-   len		:: "'a list => nat"
-   at		:: "['a list, nat] => 'a"
-   "[]"		:: "'a list"	("[]")
-   "."		:: "['a, 'a list] => 'a list"  (infixr 80)
-   "++"		:: "['a list, 'a list] => 'a list" (infixr 70)
+   hd		:: 'a list => 'a  
+   tl		:: 'a list => 'a list
+   forall	:: ['a list, 'a => o] => o  
+   len		:: 'a list => nat  
+   at		:: ['a list, nat] => 'a  
+   "[]"		:: ('a list)  	                     ("[]")
+   "."		:: ['a, 'a list] => 'a list          (infixr 80)
+   "++"		:: ['a list, 'a list] => 'a list     (infixr 70)
 
 rules
  list_ind "[| P([]);  ALL x l. P(l)-->P(x.l) |] ==> All(P)"