Replacing the primrec definition of "length" by a translation to the built-in
"size" function

--- a/src/HOL/List.thy	Fri Jun 13 10:35:13 1997 +0200
+++ b/src/HOL/List.thy	Mon Jun 16 14:24:11 1997 +0200
@@ -16,7 +16,6 @@
   concat      :: 'a list list => 'a list
   foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
   hd          :: 'a list => 'a
-  length      :: 'a list => nat
   set_of_list :: 'a list => 'a set
   list_all    :: ('a => bool) => ('a list => bool)
   map         :: ('a=>'b) => ('a list => 'b list)
@@ -53,6 +52,11 @@
     Cons "[| a: A;  l: lists A |] ==> a#l : lists A"
 
 
+(*Function "size" is overloaded for all datatypes.  Users may refer to the
+  list version as "length".*)
+syntax   length :: 'a list => nat
+translations  "length"  =>  "size"
+
 primrec hd list
   "hd([]) = arbitrary"
   "hd(x#xs) = x"
@@ -87,9 +91,6 @@
 primrec foldl list
   "foldl f a [] = a"
   "foldl f a (x#xs) = foldl f (f a x) xs"
-primrec length list
-  "length([]) = 0"
-  "length(x#xs) = Suc(length(xs))"
 primrec concat list
   "concat([]) = []"
   "concat(x#xs) = x @ concat(xs)"