src/HOL/Tools/lin_arith.ML
changeset 52131 366fa32ee2a3
parent 51717 9e7d1c139569
child 54249 ce00f2fef556
     1.1 --- a/src/HOL/Tools/lin_arith.ML	Fri May 24 16:42:57 2013 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri May 24 17:00:46 2013 +0200
     1.3 @@ -125,9 +125,9 @@
     1.4  
     1.5  fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) :
     1.6               (term * Rat.rat) list * Rat.rat =
     1.7 -  case AList.lookup Pattern.aeconv p t of
     1.8 +  case AList.lookup Envir.aeconv p t of
     1.9        NONE   => ((t, m) :: p, i)
    1.10 -    | SOME n => (AList.update Pattern.aeconv (t, Rat.add n m) p, i);
    1.11 +    | SOME n => (AList.update Envir.aeconv (t, Rat.add n m) p, i);
    1.12  
    1.13  (* decompose nested multiplications, bracketing them to the right and combining
    1.14     all their coefficients
    1.15 @@ -320,7 +320,7 @@
    1.16  
    1.17  fun subst_term ([] : (term * term) list) (t : term) = t
    1.18    | subst_term pairs                     t          =
    1.19 -      (case AList.lookup Pattern.aeconv pairs t of
    1.20 +      (case AList.lookup Envir.aeconv pairs t of
    1.21          SOME new =>
    1.22            new
    1.23        | NONE     =>
    1.24 @@ -672,7 +672,7 @@
    1.25  fun negated_term_occurs_positively (terms : term list) : bool =
    1.26    List.exists
    1.27      (fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
    1.28 -      member Pattern.aeconv terms (Trueprop $ t)
    1.29 +      member Envir.aeconv terms (Trueprop $ t)
    1.30        | _ => false)
    1.31      terms;
    1.32