src/HOL/ex/Abstract_NAT.thy

--- a/src/HOL/ex/Abstract_NAT.thy	Wed Jul 11 11:52:00 2007 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy	Wed Jul 11 11:52:28 2007 +0200
@@ -26,7 +26,7 @@
 
 text {* \medskip Primitive recursion as a (functional) relation -- polymorphic! *}
 
-inductive2
+inductive
   Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
   for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
 where