src/HOL/List.thy

--- a/src/HOL/List.thy	Sat Jul 18 12:41:09 1998 +0200
+++ b/src/HOL/List.thy	Mon Jul 20 16:04:53 1998 +0200
@@ -99,8 +99,8 @@
   "map f [] = []"
   "map f (x#xs) = f(x)#map f xs"
 primrec "op @" list
-  "[] @ ys = ys"
-  "(x#xs)@ys = x#(xs@ys)"
+append_Nil  "[]    @ys = ys"
+append_Cons "(x#xs)@ys = x#(xs@ys)"
 primrec rev list
   "rev([]) = []"
   "rev(x#xs) = rev(xs) @ [x]"