# HG changeset patch
# User haftmann
# Date 1256748243 -3600
# Node ID b497b2574bf67ee926cf154affd6765a5ad0f613
# Parent  b6ff7db522b555c87517c5a3ceb0abdc576174f4
load Product_Type before Nat; dropped junk

diff -r b6ff7db522b5 -r b497b2574bf6 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 28 17:44:03 2009 +0100
+++ b/src/HOL/Product_Type.thy	Wed Oct 28 17:44:03 2009 +0100
@@ -6,7 +6,7 @@
 header {* Cartesian products *}
 
 theory Product_Type
-imports Inductive Nat
+imports Inductive
 uses
   ("Tools/split_rule.ML")
   ("Tools/inductive_set.ML")
@@ -94,8 +94,6 @@
 
 text {* code generator setup *}
 
-instance unit :: eq ..
-
 lemma [code]:
   "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
 
@@ -932,8 +930,6 @@
 
 subsubsection {* Code generator setup *}
 
-instance * :: (eq, eq) eq ..
-
 lemma [code]:
   "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)