# HG changeset patch
# User wenzelm
# Date 1005175536 -3600
# Node ID 784fe681ba26f753cb93303dec6b8e4fc86aee1f
# Parent  ddb042d222193fe1fbc27780f210967c07140629
use num_const of Pure;

diff -r ddb042d22219 -r 784fe681ba26 src/HOL/Numeral.thy
--- 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