# HG changeset patch
# User berghofe
# Date 1028550560 -7200
# Node ID 278f2cba42ab1d552e8a6cfe6e40a07c76ce5a0a
# Parent  467bccacc0510ea7dc17e32a32feb8ecc8baf802
Removed reference to theory NatDef.

diff -r 467bccacc051 -r 278f2cba42ab src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Mon Aug 05 14:28:31 2002 +0200
+++ b/src/HOL/Extraction.thy	Mon Aug 05 14:29:20 2002 +0200
@@ -428,10 +428,10 @@
 qed
 
 realizers
-  NatDef.nat_induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"
+  Nat.nat_induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"
     "\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
 
-  NatDef.nat_induct: "Null"
+  Nat.nat_induct: "Null"
     "\<Lambda>P n. nat_induct \<cdot> _ \<cdot> _"
 
   Nat.nat.induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"