src/HOL/Induct/SList.thy

--- a/src/HOL/Induct/SList.thy	Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Induct/SList.thy	Sat May 19 11:33:57 2007 +0200
@@ -159,6 +159,10 @@
   map       :: "('a=>'b) => ('a list => 'b list)" where
   "map f xs = list_rec xs [] (%x l r. f(x)#r)"
 
+no_syntax
+  append :: "'a list => 'a list => 'a list" (infixr "@" 65)
+hide const "List.append"
+
 definition
   append    :: "['a list, 'a list] => 'a list"   (infixr "@" 65) where
   "xs@ys = list_rec xs ys (%x l r. x#r)"