diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Product_Type.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -764,7 +764,7 @@
 instance unit :: eq ..
 
 lemma [code func]:
-  "OperationalEquality.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
+  "Code_Generator.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
 
 code_instance unit :: eq
   (Haskell -)
@@ -772,16 +772,16 @@
 instance * :: (eq, eq) eq ..
 
 lemma [code func]:
-  "OperationalEquality.eq (x1, y1) (x2, y2) = (OperationalEquality.eq x1 x2 \<and> OperationalEquality.eq y1 y2)"
+  "Code_Generator.eq (x1, y1) (x2, y2) = (Code_Generator.eq x1 x2 \<and> Code_Generator.eq y1 y2)"
   unfolding eq_def by auto
 
 code_instance * :: eq
   (Haskell -)
 
-code_const "OperationalEquality.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+code_const "Code_Generator.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
-code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 types_code