Tuned error messages; tuned;
authorchaieb
Sun Jun 17 13:39:34 2007 +0200 (2007-06-17)
changeset 2340868d69273e522
parent 23407 0e4452fcbeb8
child 23409 1e0b49793464
Tuned error messages; tuned;
src/HOL/Tools/Presburger/cooper.ML
     1.1 --- a/src/HOL/Tools/Presburger/cooper.ML	Sun Jun 17 13:39:32 2007 +0200
     1.2 +++ b/src/HOL/Tools/Presburger/cooper.ML	Sun Jun 17 13:39:34 2007 +0200
     1.3 @@ -520,7 +520,7 @@
     1.4   fun conv ctxt p = 
     1.5    let val _ = () (* my_term := p *)
     1.6    in
     1.7 -   Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) 
     1.8 +   Qelim.gen_qelim_conv ctxt pcv postcv pcv (cons o term_of) 
     1.9        (term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
    1.10        (cooperex_conv ctxt) p 
    1.11    end
    1.12 @@ -552,9 +552,9 @@
    1.13  	     (Mul (HOLogic.dest_number t1 |> snd |> Integer.machine_int,i_of_term vs t2)
    1.14          handle TERM _ => 
    1.15             (Mul (HOLogic.dest_number t2 |> snd |> Integer.machine_int,i_of_term vs t1)
    1.16 -            handle TERM _ => cooper "i_of_term: Unsupported kind of multiplication"))
    1.17 +            handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
    1.18        | _ => (C (HOLogic.dest_number t |> snd |> Integer.machine_int) 
    1.19 -               handle TERM _ => cooper "i_of_term: unknown term");
    1.20 +               handle TERM _ => cooper "Reification: unknown term");
    1.21  	
    1.22  fun qf_of_term ps vs t = 
    1.23      case t of 
    1.24 @@ -563,7 +563,7 @@
    1.25        | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
    1.26        | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
    1.27        | Const(@{const_name "Divides.dvd"},_)$t1$t2 => 
    1.28 -	(Dvd(HOLogic.dest_number t1 |> snd |> Integer.machine_int, i_of_term vs t2) handle _ => cooper "qf_of_term: unsupported dvd")
    1.29 +	(Dvd(HOLogic.dest_number t1 |> snd |> Integer.machine_int, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
    1.30        | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    1.31        | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.32        | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.33 @@ -581,7 +581,7 @@
    1.34           in A (qf_of_term ps vs' p')
    1.35           end
    1.36        | _ =>(case AList.lookup (op aconv) ps t of 
    1.37 -               NONE => cooper "qf_of_term ps : unknown term!"
    1.38 +               NONE => cooper "Reification: unknown term!"
    1.39               | SOME n => Closed n);
    1.40  
    1.41  local