src/HOL/Tools/Qelim/cooper.ML
changeset 32398 40a0760a00ea
parent 32264 0be31453f698
child 32429 54758ca53fd6
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Aug 24 09:49:50 2009 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Aug 24 10:44:03 2009 +0200
     1.3 @@ -246,8 +246,10 @@
     1.4               RS eq_reflection
     1.5  end;
     1.6  
     1.7 -fun is_intrel (b$_$_) = domain_type (fastype_of b) = HOLogic.intT
     1.8 -  | is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT
     1.9 +fun is_intrel_type T = T = @{typ "int => int => bool"};
    1.10 +
    1.11 +fun is_intrel (b$_$_) = is_intrel_type (fastype_of b)
    1.12 +  | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b)
    1.13    | is_intrel _ = false;
    1.14   
    1.15  fun linearize_conv ctxt vs ct = case term_of ct of