--- 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)