--- a/src/HOL/ex/NatSum.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/NatSum.thy Fri Jul 24 13:19:38 1998 +0200
@@ -8,7 +8,7 @@
NatSum = Arith +
consts sum :: [nat=>nat, nat] => nat
-primrec "sum" nat
+primrec
"sum f 0 = 0"
"sum f (Suc n) = f(n) + sum f n"