diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Datatype.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -8,10 +8,6 @@
 theory Datatype
 imports Product_Type Sum_Type Nat
 keywords "datatype" :: thy_decl
-uses
-  ("Tools/Datatype/datatype.ML")
-  ("Tools/inductive_realizer.ML")
-  ("Tools/Datatype/datatype_realizer.ML")
 begin
 
 subsection {* The datatype universe *}
@@ -517,12 +513,12 @@
 hide_type (open) node item
 hide_const (open) Push Node Atom Leaf Numb Lim Split Case
 
-use "Tools/Datatype/datatype.ML"
+ML_file "Tools/Datatype/datatype.ML"
 
-use "Tools/inductive_realizer.ML"
+ML_file "Tools/inductive_realizer.ML"
 setup InductiveRealizer.setup
 
-use "Tools/Datatype/datatype_realizer.ML"
+ML_file "Tools/Datatype/datatype_realizer.ML"
 setup Datatype_Realizer.setup
 
 end