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;