# HG changeset patch
# User boehmes
# Date 1251103443 -7200
# Node ID 40a0760a00eab73815e51b840fecfec6e8d5be7e
# Parent  1899b8c47961c864e2369e20f475d28a05e66df0
stricter condition for (binary) integer relation

diff -r 1899b8c47961 -r 40a0760a00ea src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon Aug 24 09:49:50 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Aug 24 10:44:03 2009 +0200
@@ -246,8 +246,10 @@
              RS eq_reflection
 end;
 
-fun is_intrel (b$_$_) = domain_type (fastype_of b) = HOLogic.intT
-  | is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT
+fun is_intrel_type T = T = @{typ "int => int => bool"};
+
+fun is_intrel (b$_$_) = is_intrel_type (fastype_of b)
+  | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b)
   | is_intrel _ = false;
  
 fun linearize_conv ctxt vs ct = case term_of ct of