# [isabelle] [Isabelle2016-1-RC4] Simplification of numerals very slow when Primes is imported

Dear all,
while updating some of my theories to Isabelle2016-1, I noticed that simplification of some goals
involving numerals is extremely slow when the "Primes" theory is imported. In the attachment, you
can find a small theory containing two applications of "simp". When the Primes theory is loaded,
the first application takes about a minute to complete, whereas the second one returns almost
immediately. When importing Main instead of Primes, both invocations of simp are equally fast.
I did not observe this behaviour with Isabelle2016. Does anyone have an idea what is going wrong?
Perhaps the simpset got messed up during the recent update of the number theory library?
Greetings,
Stefan

theory Slow
imports "~~/src/HOL/Number_Theory/Primes"
begin
(* very slow when Primes theory is loaded *)
lemma "((foo::int) + bar * xxx mod 2 ^ 8) mod 2 ^ 8 = baz"
apply simp
oops
(* this one is faster *)
lemma "((foo::int) + bar * xxx) mod 2 ^ 8 = baz"
apply simp
oops
end

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*