1.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Jun 21 12:33:43 2010 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Jun 21 13:35:10 2010 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4  
     1.5  lemma "make_point_ext_type (dest_point_ext_type a) = a"
     1.6  nitpick [expect = none]
     1.7 -by (rule Rep_point_ext_type_inverse)
     1.8 +by (rule dest_point_ext_type_inverse)
     1.9  
    1.10  lemma "Fract a b = of_int a / of_int b"
    1.11  nitpick [card = 1, expect = none]