src/Provers/Arith/cancel_div_mod.ML

   let val ts = Data.dest_sum t;
       val dpq = Data.mk_binop Data.div_name pq
       val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
       val d = if d1 mem ts then d1 else d2
       val m = Data.mk_binop Data.mod_name pq
-  in mk_plus(mk_plus(d,m),Data.mk_sum(ts \ d \ m)) end
+  in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end
 
 fun cancel ss t pq =
   let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
   in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;