# HG changeset patch
# User blanchet
# Date 1336690956 -7200
# Node ID ca5b629a59957265dfb9697f1745cb17cb348def
# Parent  5f1afeebafbc372ffb8f0cf6c4bc87deb802fd28
reintroduced example now that it's no longer broken

diff -r 5f1afeebafbc -r ca5b629a5995 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"