src/HOL/Transfer.thy

--- a/src/HOL/Transfer.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Transfer.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -6,7 +6,6 @@
 
 theory Transfer
 imports Plain Hilbert_Choice
-uses ("Tools/transfer.ML")
 begin
 
 subsection {* Relator for function space *}
@@ -96,8 +95,7 @@
   shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
   using assms unfolding Rel_def fun_rel_def by fast
 
-use "Tools/transfer.ML"
-
+ML_file "Tools/transfer.ML"
 setup Transfer.setup
 
 declare fun_rel_eq [relator_eq]