# HG changeset patch
# User wenzelm
# Date 1183586769 -7200
# Node ID b3ce27bd211f375d660e0ce575c33d7ee1c21a2d
# Parent  0cd175710a9328ca20e8f11ec079384ac41c5edf
Numeral.mk_cnumber;

diff -r 0cd175710a93 -r b3ce27bd211f src/HOL/Arith_Tools.thy
--- a/src/HOL/Arith_Tools.thy	Wed Jul 04 21:20:23 2007 +0200
+++ b/src/HOL/Arith_Tools.thy	Thu Jul 05 00:06:09 2007 +0200
@@ -591,11 +591,11 @@
 
 fun mk_const phi cT x =
  let val (a, b) = Rat.quotient_of_rat x
- in if b = 1 then Normalizer.mk_cnumber cT a
+ in if b = 1 then Numeral.mk_cnumber cT a
     else Thm.capply
          (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
-                     (Normalizer.mk_cnumber cT a))
-         (Normalizer.mk_cnumber cT b)
+                     (Numeral.mk_cnumber cT a))
+         (Numeral.mk_cnumber cT b)
   end
 
 in
@@ -723,11 +723,11 @@
 
 fun mk_frac phi cT x =
  let val (a, b) = Rat.quotient_of_rat x
- in if b = 1 then Normalizer.mk_cnumber cT a
+ in if b = 1 then Numeral.mk_cnumber cT a
     else Thm.capply
          (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
-                     (Normalizer.mk_cnumber cT a))
-         (Normalizer.mk_cnumber cT b)
+                     (Numeral.mk_cnumber cT a))
+         (Numeral.mk_cnumber cT b)
  end
 
 fun whatis x ct = case term_of ct of