
diff -r f92919b141b2 -r 42ff710d432f src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Feb 25 15:19:19 2006 +0100
+++ b/src/HOL/List.thy	Sat Feb 25 15:19:47 2006 +0100
@@ -2691,6 +2691,8 @@
   "List.op @" "List.append"
   "List.op mem" "List.member"
 
+code_generate Nil Cons
+
 code_syntax_tyco
   list
     ml ("_ list")




