--- a/src/HOL/Sum_Type.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Sum_Type.thy Thu Sep 11 18:54:36 2014 +0200
@@ -90,11 +90,11 @@
| Inr projr
by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
-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 Inl Inr
+old_rep_datatype Inl Inr
proof -
fix P
fix s :: "'a + 'b"