src/Provers/Arith/fast_lin_arith.ML
changeset 52131 366fa32ee2a3
parent 51930 52fd62618631
child 55362 5e5c36b051af
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri May 24 16:42:57 2013 +0200
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri May 24 17:00:46 2013 +0200
     1.3 @@ -458,8 +458,8 @@
     1.4  fun trace_msg ctxt msg =
     1.5    if Config.get ctxt LA_Data.trace then tracing msg else ();
     1.6  
     1.7 -val union_term = union Pattern.aeconv;
     1.8 -val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
     1.9 +val union_term = union Envir.aeconv;
    1.10 +val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Envir.aeconv (t, t'));
    1.11  
    1.12  fun add_atoms (lhs, _, _, rhs, _, _) =
    1.13    union_term (map fst lhs) o union_term (map fst rhs);
    1.14 @@ -572,7 +572,7 @@
    1.15  end;
    1.16  
    1.17  fun coeff poly atom =
    1.18 -  AList.lookup Pattern.aeconv poly atom |> the_default 0;
    1.19 +  AList.lookup Envir.aeconv poly atom |> the_default 0;
    1.20  
    1.21  fun integ(rlhs,r,rel,rrhs,s,d) =
    1.22  let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s