# HG changeset patch
# User wenzelm
# Date 1414770983 -3600
# Node ID c44aff8ac8940a78e28d653f0ecf8d3e7fb700bc
# Parent  98c03412079b6ec04beca6b7f62f23827b3c4c00
avoid noise (cf. 03ff4d1e6784);

diff -r 98c03412079b -r c44aff8ac894 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Oct 31 16:03:45 2014 +0100
+++ b/src/HOL/Divides.thy	Fri Oct 31 16:56:23 2014 +0100
@@ -2047,8 +2047,8 @@
   val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
   val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
   val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]
-  fun prove ctxt goal = (writeln "prove"; Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
-    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps)))));
+  fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
+    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))));
   fun binary_proc proc ctxt ct =
     (case Thm.term_of ct of
       _ $ t $ u =>