src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 33212 f3c8acbff503
parent 33152 241cfaed158f
child 33268 02de0317f66f
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Oct 26 20:17:55 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Oct 26 20:41:26 2009 +0100
     1.3 @@ -2993,7 +2993,7 @@
     1.4   | Const(@{const_name "power"},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
     1.5   | Const(@{const_name "HOL.divide"},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
     1.6   | _ => (FRPar.C (HOLogic.dest_number t |> snd,1) 
     1.7 -         handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> valOf));
     1.8 +         handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> the));
     1.9  
    1.10  fun tm_of_term m m' t = 
    1.11   case t of
    1.12 @@ -3002,14 +3002,14 @@
    1.13   | Const(@{const_name "HOL.minus"},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
    1.14   | Const(@{const_name "HOL.times"},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
    1.15   | _ => (FRPar.CP (num_of_term m' t) 
    1.16 -         handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> valOf)
    1.17 -              | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> valOf));
    1.18 +         handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the)
    1.19 +              | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the));
    1.20  
    1.21  fun term_of_num T m t = 
    1.22   case t of
    1.23    FRPar.C (a,b) => (if b = 1 then num T a else if b=0 then (rz T) 
    1.24                                          else (divt T) $ num T a $ num T b)
    1.25 -| FRPar.Bound i => AList.lookup (op = : int*int -> bool) m i |> valOf
    1.26 +| FRPar.Bound i => AList.lookup (op = : int*int -> bool) m i |> the
    1.27  | FRPar.Add(a,b) => (plust T)$(term_of_num T m a)$(term_of_num T m b)
    1.28  | FRPar.Mul(a,b) => (timest T)$(term_of_num T m a)$(term_of_num T m b)
    1.29  | FRPar.Sub(a,b) => (minust T)$(term_of_num T m a)$(term_of_num T m b)
    1.30 @@ -3021,7 +3021,7 @@
    1.31  fun term_of_tm T m m' t = 
    1.32   case t of
    1.33    FRPar.CP p => term_of_num T m' p
    1.34 -| FRPar.tm_Bound i => AList.lookup (op = : int*int -> bool) m i |> valOf
    1.35 +| FRPar.tm_Bound i => AList.lookup (op = : int*int -> bool) m i |> the
    1.36  | FRPar.tm_Add(a,b) => (plust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
    1.37  | FRPar.tm_Mul(a,b) => (timest T)$(term_of_num T m' a)$(term_of_tm T m m' b)
    1.38  | FRPar.tm_Sub(a,b) => (minust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)