diff -r af32e2c3f77a -r a6922171b396 src/HOL/List.thy
--- a/src/HOL/List.thy Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/List.thy Tue Jan 19 11:18:11 1999 +0100
@@ -114,8 +114,8 @@
"filter P [] = []"
"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
primrec
- "foldl f a [] = a"
- "foldl f a (x#xs) = foldl f (f a x) xs"
+ foldl_Nil "foldl f a [] = a"
+ foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
primrec
"concat([]) = []"
"concat(x#xs) = x @ concat(xs)"