--- 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)