# HG changeset patch
# User paulson
# Date 1011606725 -3600
# Node ID 2f61bca07de77beb5ed0754de816345a194c26fe
# Parent  e7b4c0731d57f3b043da0a38d83e0020f5e8328f
slight re-use of code

diff -r e7b4c0731d57 -r 2f61bca07de7 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Sat Jan 19 15:44:53 2002 +0100
+++ b/src/HOL/Real/RealBin.ML	Mon Jan 21 10:52:05 2002 +0100
@@ -269,17 +269,8 @@
 fun mk_numeral n = HOLogic.number_of_const HOLogic.realT $ HOLogic.mk_bin n;
 
 (*Decodes a binary real constant, or 0, 1*)
-fun dest_numeral (Const("0", _)) = 0
-  | dest_numeral (Const("1", _)) = 1
-  | dest_numeral (Const("Numeral.number_of", _) $ w) = 
-     (HOLogic.dest_binum w
-      handle TERM _ => raise TERM("Real_Numeral_Simprocs.dest_numeral:1", [w]))
-  | dest_numeral t = raise TERM("Real_Numeral_Simprocs.dest_numeral:2", [t]);
-
-fun find_first_numeral past (t::terms) =
-	((dest_numeral t, rev past @ terms)
-	 handle TERM _ => find_first_numeral (t::past) terms)
-  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
+val dest_numeral = Int_Numeral_Simprocs.dest_numeral;
+val find_first_numeral = Int_Numeral_Simprocs.find_first_numeral;
 
 val zero = mk_numeral 0;
 val mk_plus = HOLogic.mk_binop "op +";