1.1 --- a/src/HOL/Integ/cooper_dec.ML	Sun Aug 29 17:42:11 2004 +0200
     1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Mon Aug 30 12:01:52 2004 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    val is_arith_rel : term -> bool
     1.5    val mk_numeral : int -> term
     1.6    val dest_numeral : term -> int
     1.7 +  val is_numeral : term -> bool
     1.8    val zero : term
     1.9    val one : term
    1.10    val linear_cmul : int -> term -> term
    1.11 @@ -208,10 +209,13 @@
    1.12   
    1.13  fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); 
    1.14   
    1.15 -fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =  
    1.16 +fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =
    1.17 +    if is_numeral c then   
    1.18        let val c' = (mk_numeral(abs(dest_numeral c)))  
    1.19        in (HOLogic.mk_binrel "Divides.op dvd" (c,lint vars t)) 
    1.20        end 
    1.21 +    else (warning "Nonlinear term --- Non numeral leftside at dvd"
    1.22 +      ;raise COOPER)
    1.23    |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
    1.24    |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
    1.25    |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))