diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Record.thy --- a/src/HOL/Record.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Record.thy Wed Aug 22 22:55:41 2012 +0200 @@ -11,7 +11,6 @@ theory Record imports Plain Quickcheck_Narrowing keywords "record" :: thy_decl -uses ("Tools/record.ML") begin subsection {* Introduction *} @@ -461,7 +460,7 @@ subsection {* Record package *} -use "Tools/record.ML" setup Record.setup +ML_file "Tools/record.ML" setup Record.setup hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons