# HG changeset patch
# User nipkow
# Date 868445824 -7200
# Node ID 157be29ad5ba132356a6e8f0c0a46386a76f865e
# Parent  a36e0a49d2cd06f9ae8c4b1ad0411da9bef0d78d
Improved length = size translation.

diff -r a36e0a49d2cd -r 157be29ad5ba src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jul 07 10:49:14 1997 +0200
+++ b/src/HOL/List.thy	Wed Jul 09 12:57:04 1997 +0200
@@ -55,7 +55,7 @@
 (*Function "size" is overloaded for all datatypes.  Users may refer to the
   list version as "length".*)
 syntax   length :: 'a list => nat
-translations  "length"  =>  "size"
+translations  "length"  =>  "size:: _ list => nat"
 
 primrec hd list
   "hd([]) = arbitrary"
@@ -111,3 +111,19 @@
   "dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)"
 
 end
+
+ML
+
+local
+
+(* translating size::list -> length *)
+
+fun size_tr' (Type ("fun", (Type ("list", _) :: _))) [t] =
+      Syntax.const "length" $ t
+  | size_tr'   _ _ = raise Match;
+
+in
+
+val typed_print_translation = [("size", size_tr')];
+
+end;