diff -r f30b73385060 -r 25b068a99d2b src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -193,6 +193,8 @@
   then show ?thesis by auto
 qed
 
+ML {* fast_arith_split_limit := 0; *} (*FIXME*)
+
 lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
     (p * b \<noteq> q * a)"
 proof
@@ -234,6 +236,8 @@
   with q_g_2 show False by auto
 qed
 
+ML {* fast_arith_split_limit := 9; *} (*FIXME*)
+
 lemma (in QRTEMP) P_set_finite: "finite (P_set)"
   using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)