diff -r af4c18c30593 -r 544867142ea4 src/ZF/List_ZF.thy
--- a/src/ZF/List_ZF.thy	Wed Feb 10 00:45:16 2010 +0100
+++ b/src/ZF/List_ZF.thy	Wed Feb 10 00:46:56 2010 +0100
@@ -19,9 +19,9 @@
  "@List"     :: "is => i"                                 ("[(_)]")
 
 translations
-  "[x, xs]"     == "Cons(x, [xs])"
-  "[x]"         == "Cons(x, [])"
-  "[]"          == "Nil"
+  "[x, xs]"     == "CONST Cons(x, [xs])"
+  "[x]"         == "CONST Cons(x, [])"
+  "[]"          == "CONST Nil"
 
 
 consts