src/HOL/ex/NatSum.thy

--- a/src/HOL/ex/NatSum.thy	Wed May 21 10:54:10 1997 +0200
+++ b/src/HOL/ex/NatSum.thy	Wed May 21 10:55:21 1997 +0200
@@ -8,6 +8,8 @@
 
 NatSum = Arith +
 consts sum     :: [nat=>nat, nat] => nat
-rules  sum_0      "sum f 0 = 0"
-       sum_Suc    "sum f (Suc n) = f(n) + sum f n"
+primrec "sum" nat 
+  "sum f 0 = 0"
+  "sum f (Suc n) = f(n) + sum f n"
+
 end