| changeset 55413 | a8e96847523c |
| parent 49187 | 6096da55d2d6 |
| child 56243 | 2e10a36b8d46 |
--- a/src/HOL/Library/Countable.thy Wed Feb 12 08:35:56 2014 +0100 +++ b/src/HOL/Library/Countable.thy Wed Feb 12 08:35:56 2014 +0100 @@ -90,7 +90,7 @@ text {* Options *} instance option :: (countable) countable - by (rule countable_classI [of "option_case 0 (Suc \<circ> to_nat)"]) + by (rule countable_classI [of "case_option 0 (Suc \<circ> to_nat)"]) (simp split: option.split_asm)