diff -r 3eac428cdd1b -r 20fa49e610ca src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Mon Feb 24 16:12:24 1997 +0100
+++ b/src/HOL/NatDef.ML	Tue Feb 25 15:05:14 1997 +0100
@@ -682,3 +682,10 @@
   "[| (m::nat) ~= n; m < n ==> P; n < m ==> P |] ==> P"
   (fn major::prems => [cut_facts_tac [less_linear] 1,
                        REPEAT(eresolve_tac ([disjE,major RS notE]@prems) 1)]);
+
+
+
+(* add function nat_add_primrec *) 
+val (_, nat_add_primrec) = Datatype.add_datatype
+([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([], "nat")], NoSyn)]) HOL.thy;
+