diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Product_Type.thy	Thu Sep 11 18:54:36 2014 +0200
@@ -15,11 +15,11 @@
 free_constructors case_bool for True | False
   by auto
 
-text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
 
 setup {* Sign.mandatory_path "old" *}
 
-rep_datatype True False by (auto intro: bool_induct)
+old_rep_datatype True False by (auto intro: bool_induct)
 
 setup {* Sign.parent_path *}
 
@@ -84,11 +84,11 @@
 free_constructors case_unit for "()"
   by auto
 
-text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
 
 setup {* Sign.mandatory_path "old" *}
 
-rep_datatype "()" by simp
+old_rep_datatype "()" by simp
 
 setup {* Sign.parent_path *}
 
@@ -257,11 +257,11 @@
     by (simp add: Pair_def Abs_prod_inject)
 qed
 
-text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
 
 setup {* Sign.mandatory_path "old" *}
 
-rep_datatype Pair
+old_rep_datatype Pair
 by (erule prod_cases) (rule prod.inject)
 
 setup {* Sign.parent_path *}