--- a/src/HOL/ex/NatSum.thy	Mon May 08 16:59:02 2000 +0200
+++ b/src/HOL/ex/NatSum.thy	Mon May 08 16:59:18 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/natsum.thy
+(*  Title:      HOL/ex/NatSum.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
@@ -9,7 +9,7 @@
 NatSum = Main +
 consts sum     :: [nat=>nat, nat] => nat
 primrec 
-  "sum f 0 = 0"
-  "sum f (Suc n) = f(n) + sum f n"
+  sum_0    "sum f 0 = 0"
+  sum_Suc  "sum f (Suc n) = f(n) + sum f n"
 
 end