oracle raises CooperDec.COOPER instead of COOPER (this is eliminated). Erronous old behaviour due to this exception is now correcrted.

--- a/src/HOL/Integ/reflected_cooper.ML	Thu Nov 09 21:44:35 2006 +0100
+++ b/src/HOL/Integ/reflected_cooper.ML	Thu Nov 09 23:33:55 2006 +0100
@@ -110,14 +110,12 @@
       | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
 
 (* The oracle *)
- exception COOPER; 
-
 fun presburger_oracle thy t =
     let val vs = start_vs t
 	val result = lift_un (term_of_qf vs) (pa (qf_of_term vs t))
     in 
     case result of 
-	None => raise COOPER
+	None => raise CooperDec.COOPER
       | Some t' => HOLogic.mk_Trueprop (HOLogic.mk_eq(t,t'))
     end ;
  

--- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Thu Nov 09 21:44:35 2006 +0100
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Thu Nov 09 23:33:55 2006 +0100
@@ -110,14 +110,12 @@
       | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
 
 (* The oracle *)
- exception COOPER; 
-
 fun presburger_oracle thy t =
     let val vs = start_vs t
 	val result = lift_un (term_of_qf vs) (pa (qf_of_term vs t))
     in 
     case result of 
-	None => raise COOPER
+	None => raise CooperDec.COOPER
       | Some t' => HOLogic.mk_Trueprop (HOLogic.mk_eq(t,t'))
     end ;