src/HOL/NSA/StarDef.thy

--- a/src/HOL/NSA/StarDef.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -6,7 +6,6 @@
 
 theory StarDef
 imports Filter
-uses ("transfer.ML")
 begin
 
 subsection {* A Free Ultrafilter over the Naturals *}
@@ -88,7 +87,7 @@
 by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
 
 text {*Initialize transfer tactic.*}
-use "transfer.ML"
+ML_file "transfer.ML"
 setup Transfer_Principle.setup
 
 method_setup transfer = {*