src/HOL/ex/Recdefs.thy

--- a/src/HOL/ex/Recdefs.thy	Thu Apr 22 13:03:46 1999 +0200
+++ b/src/HOL/ex/Recdefs.thy	Thu Apr 22 13:04:23 1999 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Recdef.thy
+(*  Title:      HOL/ex/Recdefs.thy
     ID:         $Id$
     Author:     Konrad Slind and Lawrence C Paulson
     Copyright   1996  University of Cambridge
@@ -95,7 +95,7 @@
 *)
 consts mapf :: nat => nat list
 recdef mapf "measure(%m. m)"
-congs "[map_cong]"
+congs map_cong
 "mapf 0 = []"
 "mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"