# HG changeset patch
# User haftmann
# Date 1282143576 -7200
# Node ID c9599ce8cbfceea1bf761db7647809a2cdce3127
# Parent  9cfafdb56749201025f0f511bf6236390ce841e2
adjusted to restored naming convention of logical record types

diff -r 9cfafdb56749 -r c9599ce8cbfc src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Wed Aug 18 16:59:36 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Wed Aug 18 16:59:36 2010 +0200
@@ -174,9 +174,9 @@
   Xcoord :: int
   Ycoord :: int
 
-lemma "make_point_ext_type (dest_point_ext_type a) = a"
+lemma "Abs_point_ext (Rep_point_ext a) = a"
 nitpick [expect = none]
-by (rule dest_point_ext_type_inverse)
+by (fact Rep_point_ext_inverse)
 
 lemma "Fract a b = of_int a / of_int b"
 nitpick [card = 1, expect = none]