fixed term_constants (impact on is_relevant); terms in generalize_tac are sorted before we abstract over them (to *try* to avoid the case when a term to be abstracted over already occurs in an other)
authorchaieb
Thu Jun 14 22:59:42 2007 +0200 (2007-06-14)
changeset 233924b03e3586f7f
parent 23391 a7c128816edc
child 23393 31781b2de73d
fixed term_constants (impact on is_relevant); terms in generalize_tac are sorted before we abstract over them (to *try* to avoid the case when a term to be abstracted over already occurs in an other)
src/HOL/Tools/Presburger/presburger.ML
     1.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Thu Jun 14 22:59:40 2007 +0200
     1.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Jun 14 22:59:42 2007 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  (*  Title:      HOL/Tools/Presburger/presburger.ML
     1.6      ID:         $Id$
     1.7      Author:     Amine Chaieb, TU Muenchen
     1.8 @@ -64,7 +65,7 @@
     1.9  
    1.10   val term_constants =
    1.11    let fun h acc t = case t of
    1.12 -    Const _ => [t]
    1.13 +    Const _ => insert (op aconv) t acc
    1.14    | a$b => h (h acc a) b
    1.15    | Abs (_,_,t) => h acc t
    1.16    | _ => acc
    1.17 @@ -93,7 +94,7 @@
    1.18     let 
    1.19     fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
    1.20     fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
    1.21 -   val ts = f p
    1.22 +   val ts = sort (fn (a,b) => Term.fast_term_ord (term_of a, term_of b)) (f p)
    1.23     val p' = fold_rev gen ts p
    1.24   in Seq.of_list [implies_intr p' (implies_elim st (fold forall_elim ts (assume p')))]
    1.25   end;
    1.26 @@ -179,7 +180,7 @@
    1.27     NONE => all_tac st
    1.28   | SOME _ => (if q then I else TRY) (rtac TrueI i) st
    1.29  
    1.30 -fun cooper_tac elim add_ths del_ths = fn ctxt => fn i => 
    1.31 +fun cooper_tac elim add_ths del_ths ctxt i = 
    1.32  let val ss = fst (Cooper_Data.get ctxt) delsimps del_ths addsimps add_ths
    1.33  in
    1.34  nogoal_tac i