diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Thu Mar 06 15:25:21 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Thu Mar 06 15:29:18 2014 +0100
@@ -1565,7 +1565,7 @@
     using the same attribute. For example:
 
     @{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\
-    @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (prod_rel A B)"}
+    @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)"}
 
   \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
     of rules, which specify a domain of a transfer relation by a predicate.