# HG changeset patch
# User chaieb
# Date 1163111635 -3600
# Node ID 9442e9d75ada8a9a9dbad6b1403bebe14e6776f8
# Parent  ac2d7e03a3b1b46e09375b224e0010a219b67b49
oracle raises CooperDec.COOPER instead of COOPER (this is eliminated). Erronous old behaviour due to this exception is now correcrted.

diff -r ac2d7e03a3b1 -r 9442e9d75ada src/HOL/Integ/reflected_cooper.ML
--- 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 ;
  
diff -r ac2d7e03a3b1 -r 9442e9d75ada src/HOL/Tools/Presburger/reflected_cooper.ML
--- 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 ;