--- a/src/HOL/Tools/Qelim/presburger.ML Tue Oct 20 16:13:01 2009 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML Wed Oct 21 08:14:38 2009 +0200
@@ -84,7 +84,7 @@
in h [] end;
in
fun is_relevant ctxt ct =
- gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
+ subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct))
andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct));