# HG changeset patch
# User chaieb
# Date 1199570729 -3600
# Node ID af0c90f54ebe10d392c6f8e8252625d23d0f7e9b
# Parent  fdabeed7ccd9f79f5486e8a1bb19c5c929f993b3
Tuned relevant premises selection

diff -r fdabeed7ccd9 -r af0c90f54ebe src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Sat Jan 05 21:57:18 2008 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Sat Jan 05 23:05:29 2008 +0100
@@ -68,7 +68,7 @@
  | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
 
  fun ty cts t = 
- if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT]) then false 
+ if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT, HOLogic.boolT]) then false 
     else case term_of t of 
       c$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}] 
                then not (isnum l orelse isnum r)
@@ -170,6 +170,7 @@
   THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   THEN_ALL_NEW simp_tac ss
   THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
+  THEN_ALL_NEW ObjectLogic.full_atomize_tac
   THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
   THEN_ALL_NEW ObjectLogic.full_atomize_tac
   THEN_ALL_NEW div_mod_tac ctxt