src/HOL/Num.thy

--- a/src/HOL/Num.thy	Fri Mar 30 16:43:07 2012 +0200
+++ b/src/HOL/Num.thy	Fri Mar 30 16:44:23 2012 +0200
@@ -7,6 +7,8 @@
 
 theory Num
 imports Datatype
+uses
+  ("Tools/numeral.ML")
 begin
 
 subsection {* The @{text num} type *}
@@ -331,6 +333,9 @@
     (@{const_syntax neg_numeral}, num_tr' "-")] end
 *}
 
+use "Tools/numeral.ML"
+
+
 subsection {* Class-specific numeral rules *}
 
 text {*