src/HOL/Nitpick_Examples/Typedef_Nits.thy

--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri May 11 00:45:24 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri May 11 01:02:36 2012 +0200
@@ -176,9 +176,7 @@
 by (fact Rep_point_ext_inverse)
 
 lemma "Fract a b = of_int a / of_int b"
-(* FIXME: broken by conversion of Rat.thy to lift_definition/transfer.
 nitpick [card = 1, expect = none]
-*)
 by (rule Fract_of_int_quotient)
 
 lemma "Abs_rat (Rep_rat a) = a"