# HG changeset patch
# User haftmann
# Date 1200901409 -3600
# Node ID 6bfef23e26beb45fc5853999f717e689fc4801eb
# Parent  042e877d984142250b56eca9d82ed6c0cad47788
avoiding direct references to numeral presentation

diff -r 042e877d9841 -r 6bfef23e26be src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Mon Jan 21 08:43:27 2008 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy	Mon Jan 21 08:43:29 2008 +0100
@@ -62,10 +62,7 @@
                       SOME v => v
                     | NONE   => insert t)
     (*abstraction of a numeric literal*)
-    fun lit (t as Const(@{const_name HOL.zero}, _)) = t
-      | lit (t as Const(@{const_name HOL.one}, _)) = t
-      | lit (t as Const(@{const_name Int.number_of}, _) $ w) = t
-      | lit t = replace t
+    fun lit t = if can HOLogic.dest_number t then t else replace t;
     (*abstraction of a real/rational expression*)
     fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
       | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)