use num_const of Pure;

--- a/src/HOL/Numeral.thy	Thu Nov 08 00:25:09 2001 +0100
+++ b/src/HOL/Numeral.thy	Thu Nov 08 00:25:36 2001 +0100
@@ -19,12 +19,8 @@
 consts
   number_of :: "bin => 'a::number"
 
-nonterminals
-  numeral
-
 syntax
-  "_constify" :: "num => numeral"    ("_")
-  "_Numeral" :: "numeral => 'a"    ("_")
+  "_Numeral" :: "num_const => 'a"    ("_")
   Numeral0 :: 'a
   Numeral1 :: 'a