diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/HOL/Basic_BNFs.thy
--- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:25:21 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:29:18 2014 +0100
@@ -104,19 +104,19 @@
 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
 
 definition
-  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
+  rel_prod :: "('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)"
+  "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
 
-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 rel_prod_apply [simp]:
+  "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
+  by (simp add: rel_prod_def)
 
 bnf "'a \<times> 'b"
   map: map_prod
   sets: fsts snds
   bd: natLeq
-  rel: prod_rel
+  rel: rel_prod
 proof (unfold prod_set_defs)
   show "map_prod id id = id" by (rule map_prod.id)
 next
@@ -149,13 +149,13 @@
     by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
 next
   fix R1 R2 S1 S2
-  show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
+  show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> rel_prod (R1 OO S1) (R2 OO S2)" by auto
 next
   fix R S
-  show "prod_rel R S =
+  show "rel_prod R S =
         (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
         Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
-  unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
+  unfolding prod_set_defs rel_prod_def Grp_def relcompp.simps conversep.simps fun_eq_iff
   by auto
 qed