diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Num.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -7,8 +7,6 @@
 
 theory Num
 imports Datatype
-uses
-  ("Tools/numeral.ML")
 begin
 
 subsection {* The @{text num} type *}
@@ -333,7 +331,7 @@
     (@{const_syntax neg_numeral}, num_tr' "-")] end
 *}
 
-use "Tools/numeral.ML"
+ML_file "Tools/numeral.ML"
 
 
 subsection {* Class-specific numeral rules *}