[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.