src/HOL/Sum_Type.thy
changeset 58306 117ba6cbe414
parent 58189 9d714be4f028
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Sum_Type.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Sum_Type.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -90,11 +90,11 @@
     1.4    | Inr projr
     1.5    by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
     1.6  
     1.7 -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
     1.8 +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
     1.9  
    1.10  setup {* Sign.mandatory_path "old" *}
    1.11  
    1.12 -rep_datatype Inl Inr
    1.13 +old_rep_datatype Inl Inr
    1.14  proof -
    1.15    fix P
    1.16    fix s :: "'a + 'b"