src/HOL/Tools/Qelim/cooper.ML

   val del: term list -> attribute
   val add: term list -> attribute 
   val conv: Proof.context -> conv
   val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
   val method: (Proof.context -> Method.method) context_parser
-  exception COOPER of string * exn
   val setup: theory -> theory
 end;
 
 structure Cooper: COOPER =
 struct

  | (_, _) => numeral2 Integer.add tm1 tm2;
 
 fun linear_neg tm = linear_cmul ~1 tm;
 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
 
-exception COOPER of string * exn;
-
-fun cooper s = raise COOPER ("Cooper failed", ERROR s);
+exception COOPER of string;
 
 fun lint vars tm =  if is_numeral tm then tm  else case tm of
   Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
 | Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
 | Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
 | Const (@{const_name Groups.times}, _) $ s $ t =>
   let val s' = lint vars s
       val t' = lint vars t
   in if is_numeral s' then (linear_cmul (dest_numeral s') t')
      else if is_numeral t' then (linear_cmul (dest_numeral t') s')
-     else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm]))
+     else raise COOPER "lint: not linear"
   end
  | _ => addC $ (mulC $ one $ tm) $ zero;
 
 fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Orderings.less}, T) $ s $ t)) =
     lin vs (Const (@{const_name Orderings.less_eq}, T) $ t $ s)

   in
    Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
       (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
       (cooperex_conv ctxt) p
   end
-  handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)
-        | THM s => raise COOPER ("Cooper Failed", THM s)
-        | TYPE s => raise COOPER ("Cooper Failed", TYPE s)
+  handle  CTERM s => raise COOPER "bad cterm"
+        | THM s => raise COOPER "bad thm"
+        | TYPE s => raise COOPER "bad type"
 in val conv = conv
 end;
 
 fun i_of_term vs t = case t
  of Free (xn, xT) => (case AList.lookup (op aconv) vs t
-     of NONE   => cooper "Variable not found in the list!"
+     of NONE   => raise COOPER "reification: variable not found in list"
       | SOME n => Cooper_Procedure.Bound n)
   | @{term "0::int"} => Cooper_Procedure.C 0
   | @{term "1::int"} => Cooper_Procedure.C 1
   | Term.Bound i => Cooper_Procedure.Bound i
   | Const(@{const_name Groups.uminus},_)$t' => Cooper_Procedure.Neg (i_of_term vs t')

   | Const(@{const_name Groups.minus},_)$t1$t2 => Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2)
   | Const(@{const_name Groups.times},_)$t1$t2 =>
      (Cooper_Procedure.Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
     handle TERM _ =>
        (Cooper_Procedure.Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
-        handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
+        handle TERM _ => raise COOPER "reification: unsupported kind of multiplication"))
   | _ => (Cooper_Procedure.C (HOLogic.dest_number t |> snd)
-           handle TERM _ => cooper "Reification: unknown term");
+           handle TERM _ => raise COOPER "reification: unknown term");
 
 fun qf_of_term ps vs t =  case t
  of Const("True",_) => Cooper_Procedure.T
   | Const("False",_) => Cooper_Procedure.F
   | Const(@{const_name Orderings.less},_)$t1$t2 => Cooper_Procedure.Lt (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
   | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Cooper_Procedure.Le (Cooper_Procedure.Sub(i_of_term vs t1,i_of_term vs t2))
   | Const(@{const_name Rings.dvd},_)$t1$t2 =>
-      (Cooper_Procedure.Dvd (HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle TERM _ => cooper "Reification: unsupported dvd")
+      (Cooper_Procedure.Dvd (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
+        handle TERM _ => raise COOPER "reification: unsupported dvd")
   | @{term "op = :: int => _"}$t1$t2 => Cooper_Procedure.Eq (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
   | @{term "op = :: bool => _ "}$t1$t2 => Cooper_Procedure.Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
   | Const("op &",_)$t1$t2 => Cooper_Procedure.And(qf_of_term ps vs t1,qf_of_term ps vs t2)
   | Const("op |",_)$t1$t2 => Cooper_Procedure.Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
   | Const("op -->",_)$t1$t2 => Cooper_Procedure.Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)

      let val (xn',p') = variant_abs (xn,xT,p)
          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
      in Cooper_Procedure.A (qf_of_term ps vs' p')
      end
   | _ =>(case AList.lookup (op aconv) ps t of
-           NONE => cooper "Reification: unknown term!"
+           NONE => raise COOPER "reification: unknown term"
          | SOME n => Cooper_Procedure.Closed n);
 
 local
  val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
              @{term "op = :: int => _"}, @{term "op < :: int => _"},

  | Cooper_Procedure.And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
  | Cooper_Procedure.Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
  | Cooper_Procedure.Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
  | Cooper_Procedure.Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
  | Cooper_Procedure.Closed n => the (myassoc2 ps n)
- | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n))
- | _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!";
+ | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n));
 
 fun invoke t =
   let
     val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
   in