diff -r 5d538d3d5e2a -r 2c583720436e src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Induct/SList.thy	Thu Sep 28 23:42:43 2006 +0200
@@ -73,7 +73,7 @@
 (*Declaring the abstract list constructors*)
 
 definition
-  Nil       :: "'a list"
+  Nil       :: "'a list"                               ("[]")
    "Nil  = Abs_List(NIL)"
 
   "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65)
@@ -88,19 +88,16 @@
    "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
 
 (* list Enumeration *)
-consts
-  "[]"      :: "'a list"                            ("[]")
 syntax
   "@list"   :: "args => 'a list"                    ("[(_)]")
 
 translations
   "[x, xs]" == "x#[xs]"
   "[x]"     == "x#[]"
-  "[]"      == "Nil"
 
-  "case xs of Nil => a | y#ys => b" == "list_case(a, %y ys. b, xs)"
+  "case xs of [] => a | y#ys => b" == "CONST list_case(a, %y ys. b, xs)"
 
-  
+
 (* *********************************************************************** *)
 (*                                                                         *)
 (* Generalized Map Functionals                                             *)
@@ -205,8 +202,8 @@
   "@filter"     :: "[idt, 'a list, bool] => 'a list"     ("(1[_:_ ./ _])")
 
 translations
-  "[x:xs. P]"   == "filter(%x. P) xs"
-  "Alls x:xs. P"== "list_all(%x. P)xs"
+  "[x:xs. P]" == "CONST filter(%x. P) xs"
+  "Alls x:xs. P" == "CONST list_all(%x. P)xs"
 
 
 lemma ListI: "x : list (range Leaf) ==> x : List"