# HG changeset patch
# User chaieb
# Date 1118058219 -7200
# Node ID 872ad146bb14f5c57fea4e260eb8d2f947c8e218
# Parent  8435be7188cb5ab29061d8555147aa18ede9eb32
Some error messages have been eliminated as suggested by Tobias Nipkow

diff -r 8435be7188cb -r 872ad146bb14 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Mon Jun 06 13:30:21 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Mon Jun 06 13:43:39 2005 +0200
@@ -198,9 +198,9 @@
         if is_numeral s' then (linear_cmul (dest_numeral s') t') 
         else if is_numeral t' then (linear_cmul (dest_numeral t') s') 
  
-         else (warning "lint: apparent nonlinearity"; raise COOPER)
+         else raise COOPER
          end 
-  |_ =>  error ("COOPER:lint: unknown term  \n");
+  |_ =>  raise COOPER;
    
  
  
diff -r 8435be7188cb -r 872ad146bb14 src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Mon Jun 06 13:30:21 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Mon Jun 06 13:43:39 2005 +0200
@@ -198,9 +198,9 @@
         if is_numeral s' then (linear_cmul (dest_numeral s') t') 
         else if is_numeral t' then (linear_cmul (dest_numeral t') s') 
  
-         else (warning "lint: apparent nonlinearity"; raise COOPER)
+         else raise COOPER
          end 
-  |_ =>  error ("COOPER:lint: unknown term  \n");
+  |_ =>  raise COOPER;