src/HOL/Nat_Transfer.thy

--- a/src/HOL/Nat_Transfer.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Nat_Transfer.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -5,7 +5,6 @@
 
 theory Nat_Transfer
 imports Int
-uses ("Tools/legacy_transfer.ML")
 begin
 
 subsection {* Generic transfer machinery *}
@@ -16,8 +15,7 @@
 lemma transfer_morphismI[intro]: "transfer_morphism f A"
   by (simp add: transfer_morphism_def)
 
-use "Tools/legacy_transfer.ML"
-
+ML_file "Tools/legacy_transfer.ML"
 setup Legacy_Transfer.setup