# HG changeset patch
# User wenzelm
# Date 1256403327 -7200
# Node ID 4e33c819fced368e660b296b0cc68522c0c8639f
# Parent  757d7787b10ceec0e2b50bea9949c2d17220dd33
import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);

diff -r 757d7787b10c -r 4e33c819fced src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sat Oct 24 17:49:44 2009 +0200
+++ b/src/HOL/Product_Type.thy	Sat Oct 24 18:55:27 2009 +0200
@@ -6,7 +6,7 @@
 header {* Cartesian products *}
 
 theory Product_Type
-imports Inductive
+imports Inductive Nat
 uses
   ("Tools/split_rule.ML")
   ("Tools/inductive_set.ML")