--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Oct 26 20:17:55 2009 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Oct 26 20:41:26 2009 +0100
@@ -2993,7 +2993,7 @@
| Const(@{const_name "power"},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
| Const(@{const_name "HOL.divide"},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
| _ => (FRPar.C (HOLogic.dest_number t |> snd,1)
- handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> valOf));
+ handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> the));
fun tm_of_term m m' t =
case t of
@@ -3002,14 +3002,14 @@
| Const(@{const_name "HOL.minus"},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
| Const(@{const_name "HOL.times"},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
| _ => (FRPar.CP (num_of_term m' t)
- handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> valOf)
- | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> valOf));
+ handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the)
+ | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the));
fun term_of_num T m t =
case t of
FRPar.C (a,b) => (if b = 1 then num T a else if b=0 then (rz T)
else (divt T) $ num T a $ num T b)
-| FRPar.Bound i => AList.lookup (op = : int*int -> bool) m i |> valOf
+| FRPar.Bound i => AList.lookup (op = : int*int -> bool) m i |> the
| FRPar.Add(a,b) => (plust T)$(term_of_num T m a)$(term_of_num T m b)
| FRPar.Mul(a,b) => (timest T)$(term_of_num T m a)$(term_of_num T m b)
| FRPar.Sub(a,b) => (minust T)$(term_of_num T m a)$(term_of_num T m b)
@@ -3021,7 +3021,7 @@
fun term_of_tm T m m' t =
case t of
FRPar.CP p => term_of_num T m' p
-| FRPar.tm_Bound i => AList.lookup (op = : int*int -> bool) m i |> valOf
+| FRPar.tm_Bound i => AList.lookup (op = : int*int -> bool) m i |> the
| FRPar.tm_Add(a,b) => (plust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
| FRPar.tm_Mul(a,b) => (timest T)$(term_of_num T m' a)$(term_of_tm T m m' b)
| FRPar.tm_Sub(a,b) => (minust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)