diff -r 4cc2ca4d6237 -r 048338a9b389 src/HOL/Record.thy --- a/src/HOL/Record.thy Tue Aug 17 15:17:44 2010 +0200 +++ b/src/HOL/Record.thy Tue Aug 17 15:19:37 2010 +0200 @@ -10,7 +10,7 @@ theory Record imports Plain Quickcheck -uses ("Tools/quickcheck_record.ML") ("Tools/typecopy.ML") ("Tools/record.ML") +uses ("Tools/quickcheck_record.ML") ("Tools/record.ML") begin subsection {* Introduction *} @@ -453,7 +453,6 @@ subsection {* Record package *} use "Tools/quickcheck_record.ML" -use "Tools/typecopy.ML" use "Tools/record.ML" setup Record.setup hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd