# HG changeset patch
# User blanchet
# Date 1277120110 -7200
# Node ID bd80d84b904d7c839aa5921cc620a75241950d9a
# Parent  d5a85d35ef62b247f8255be5a2f9c25bab304f58
compile

diff -r d5a85d35ef62 -r bd80d84b904d src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Jun 21 12:33:43 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Jun 21 13:35:10 2010 +0200
@@ -176,7 +176,7 @@
 
 lemma "make_point_ext_type (dest_point_ext_type a) = a"
 nitpick [expect = none]
-by (rule Rep_point_ext_type_inverse)
+by (rule dest_point_ext_type_inverse)
 
 lemma "Fract a b = of_int a / of_int b"
 nitpick [card = 1, expect = none]