src/Provers/Arith/fast_lin_arith.ML

      end handle FalseE thm => trace_thm "False reached early:" thm
   end
 end;
 
 fun coeff poly atom =
-  AList.lookup (op =) poly atom |> the_default Integer.zero;
-
-fun lcms ks = fold Integer.lcm ks Integer.one;
+  AList.lookup (op =) poly atom |> the_default (0: integer);
+
+fun lcms ks = fold Integer.lcm ks 1;
 
 fun integ(rlhs,r,rel,rrhs,s,d) =
 let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
     val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
     fun mult(t,r) =