src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Mon Aug 26 10:33:16 2013 +0200
+++ b/src/HOL/Divides.thy	Mon Aug 26 11:41:17 2013 +0200
@@ -563,7 +563,6 @@
   qed
   moreover note assms w_exhaust
   ultimately have "w = 0" by auto
-  find_theorems "_ + ?b < _ + ?b"
   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
   have "2 * (a div (2 * b)) = a div b - w"
     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)