diff -r e60036c1c248 -r 0a689157e3ce src/HOL/Lifting_Product.thy
--- a/src/HOL/Lifting_Product.thy	Mon Jan 20 20:00:33 2014 +0100
+++ b/src/HOL/Lifting_Product.thy	Mon Jan 20 20:21:12 2014 +0100
@@ -5,23 +5,14 @@
 header {* Setup for Lifting/Transfer for the product type *}
 
 theory Lifting_Product
-imports Lifting
+imports Lifting Basic_BNFs
 begin
 
 subsection {* Relator and predicator properties *}
 
-definition
-  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
-where
-  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-
 definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
 where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
 
-lemma prod_rel_apply [simp]:
-  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
-  by (simp add: prod_rel_def)
-
 lemma prod_pred_apply [simp]:
   "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
   by (simp add: prod_pred_def)