diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/List.thy
--- a/src/ZF/List.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/List.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -39,7 +39,7 @@
   "[]"          == "Nil"
 
 
-rules
+defs
 
   hd_def	"hd(l)	     == list_case(0, %x xs.x, l)"
   tl_def	"tl(l)       == list_case(Nil, %x xs.xs, l)"