# HG changeset patch
# User hoelzl
# Date 1354554803 -3600
# Node ID df5553c4973f6b6f818dbe88cb263227daff8da8
# Parent  6d5dcfb628692773932e8b4b1206dc7760b6ef98
add check to Cooper's algorithm that left-hand of dvd is a numeral

diff -r 6d5dcfb62869 -r df5553c4973f src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon Dec 03 17:18:59 2012 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Dec 03 18:13:23 2012 +0100
@@ -312,11 +312,14 @@
      then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite presburger_ss)) th
      else
      let
-      val dth =
-      ((if dest_number (term_of d') < 0 then
-          Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs)))
-                           (Thm.transitive th (inst' [d',t'] dvd_uminus))
-        else th) handle TERM _ => th)
+       val dth =
+         case perhaps_number (term_of d') of
+           SOME d => if d < 0 then
+             (Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs)))
+                              (Thm.transitive th (inst' [d',t'] dvd_uminus))
+              handle TERM _ => th)
+            else th
+         | NONE => raise COOPER "linearize_conv: not linear"
       val d'' = Thm.rhs_of dth |> Thm.dest_arg1
      in
       case tt' of