diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Typedef.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -7,7 +7,6 @@
 theory Typedef
 imports Set
 keywords "typedef" :: thy_goal and "morphisms"
-uses ("Tools/typedef.ML")
 begin
 
 locale type_definition =
@@ -109,6 +108,6 @@
 
 end
 
-use "Tools/typedef.ML" setup Typedef.setup
+ML_file "Tools/typedef.ML" setup Typedef.setup
 
 end