diff -r 04d0f732e24e -r 14d89313c66c src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Wed Mar 08 16:17:10 2000 +0100
+++ b/src/HOL/ex/NatSum.thy	Wed Mar 08 16:24:46 2000 +0100
@@ -6,7 +6,7 @@
 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
 *)
 
-NatSum = Arith +
+NatSum = Main +
 consts sum     :: [nat=>nat, nat] => nat
 primrec 
   "sum f 0 = 0"