# HG changeset patch
# User chaieb
# Date 1182080374 -7200
# Node ID 68d69273e5222cc84b7831898e47d4804cc259b5
# Parent  0e4452fcbeb84957ce6d57751ad0f74de15c7ac1
Tuned error messages; tuned;

diff -r 0e4452fcbeb8 -r 68d69273e522 src/HOL/Tools/Presburger/cooper.ML
--- a/src/HOL/Tools/Presburger/cooper.ML	Sun Jun 17 13:39:32 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper.ML	Sun Jun 17 13:39:34 2007 +0200
@@ -520,7 +520,7 @@
  fun conv ctxt p = 
   let val _ = () (* my_term := p *)
   in
-   Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) 
+   Qelim.gen_qelim_conv ctxt pcv postcv pcv (cons o term_of) 
       (term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
       (cooperex_conv ctxt) p 
   end
@@ -552,9 +552,9 @@
 	     (Mul (HOLogic.dest_number t1 |> snd |> Integer.machine_int,i_of_term vs t2)
         handle TERM _ => 
            (Mul (HOLogic.dest_number t2 |> snd |> Integer.machine_int,i_of_term vs t1)
-            handle TERM _ => cooper "i_of_term: Unsupported kind of multiplication"))
+            handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
       | _ => (C (HOLogic.dest_number t |> snd |> Integer.machine_int) 
-               handle TERM _ => cooper "i_of_term: unknown term");
+               handle TERM _ => cooper "Reification: unknown term");
 	
 fun qf_of_term ps vs t = 
     case t of 
@@ -563,7 +563,7 @@
       | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
       | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
       | Const(@{const_name "Divides.dvd"},_)$t1$t2 => 
-	(Dvd(HOLogic.dest_number t1 |> snd |> Integer.machine_int, i_of_term vs t2) handle _ => cooper "qf_of_term: unsupported dvd")
+	(Dvd(HOLogic.dest_number t1 |> snd |> Integer.machine_int, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
       | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
       | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
       | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
@@ -581,7 +581,7 @@
          in A (qf_of_term ps vs' p')
          end
       | _ =>(case AList.lookup (op aconv) ps t of 
-               NONE => cooper "qf_of_term ps : unknown term!"
+               NONE => cooper "Reification: unknown term!"
              | SOME n => Closed n);
 
 local