
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




