src/Provers/Arith/cancel_div_mod.ML

   in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
 
 fun proc ss t =
   let val (divs,mods) = coll_div_mod t ([],[])
   in if null divs orelse null mods then NONE
-     else case divs inter mods of
+     else case gen_inter (op =) (divs, mods) of
             pq :: _ => SOME (cancel ss t pq)
           | [] => NONE
   end
 
 end