# HG changeset patch
# User chaieb
# Date 1199380767 -3600
# Node ID f7c048eafa9014156a6d81fed2507bd866205716
# Parent  bac99880fa9966b30161312c3f81835f96fcdf16
tuned relevance test for presburger

diff -r bac99880fa99 -r f7c048eafa90 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Thu Jan 03 17:50:44 2008 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Thu Jan 03 18:19:27 2008 +0100
@@ -85,9 +85,9 @@
  in h [] end;
 in 
 fun is_relevant ctxt ct = 
-  gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
- andalso forall (fn Free (_,T) => T = HOLogic.intT) (term_frees (term_of ct))
- andalso forall (fn Var (_,T) => T = HOLogic.intT) (term_vars (term_of ct));
+ gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
+ andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_frees (term_of ct))
+ andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_vars (term_of ct));
 
 fun int_nat_terms ctxt ct =
  let