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