# HG changeset patch
# User wenzelm
# Date 1002536839 -7200
# Node ID 6c45813c2db1fc8e51141cb40a3554f017bd5760
# Parent  885e053ae664a6f1fc2d6dff3b76572b8396204e
replace 0r/1r by 0/1;

diff -r 885e053ae664 -r 6c45813c2db1 src/HOL/SVC_Oracle.ML
--- a/src/HOL/SVC_Oracle.ML	Mon Oct 08 12:13:56 2001 +0200
+++ b/src/HOL/SVC_Oracle.ML	Mon Oct 08 12:27:19 2001 +0200
@@ -47,8 +47,8 @@
       | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
       | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
       | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
-      | rat ((c as Const("RealDef.0r", _))) = c
-      | rat ((c as Const("RealDef.1r", _))) = c 
+      | rat ((c as Const("0", _))) = c
+      | rat ((c as Const("1", _))) = c
       | rat (t as Const("Numeral.number_of", _) $ w) = t
       | rat t = replace t
     (*abstraction of an integer expression: no div, mod*)
diff -r 885e053ae664 -r 6c45813c2db1 src/HOL/Tools/svc_funcs.ML
--- a/src/HOL/Tools/svc_funcs.ML	Mon Oct 08 12:13:56 2001 +0200
+++ b/src/HOL/Tools/svc_funcs.ML	Mon Oct 08 12:27:19 2001 +0200
@@ -155,8 +155,7 @@
     fun lit (Const("Numeral.number_of", _) $ w) =
           (HOLogic.dest_binum w handle TERM _ => raise Match)
       | lit (Const("0", _)) = 0
-      | lit (Const("RealDef.0r", _)) = 0
-      | lit (Const("RealDef.1r", _)) = 1
+      | lit (Const("1", _)) = 1
     (*translation of a literal expression [no variables]*)
     fun litExp (Const("op +", T) $ x $ y) = 
 	  if is_numeric_op T then (litExp x) + (litExp y)