# HG changeset patch
# User traytel
# Date 1471518773 -7200
# Node ID ad2c003782f9c977477b649711a715c87619ff91
# Parent  b62f4f765353b2ca0e766ba7ea9b91331349d4a3
removed debug output

diff -r b62f4f765353 -r ad2c003782f9 src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Thu Aug 18 11:10:07 2016 +0200
+++ b/src/HOL/Tools/coinduction.ML	Thu Aug 18 13:12:53 2016 +0200
@@ -50,7 +50,7 @@
           SOME raw_thms => raw_thms
         | NONE => goal |> Logic.strip_assums_concl |> find_coinduct);
       val thy = Proof_Context.theory_of ctxt;
-      val concl = Variable.focus NONE goal ctxt |> fst |> snd |> Logic.strip_imp_concl |> @{print};
+      val concl = Variable.focus NONE goal ctxt |> fst |> snd |> Logic.strip_imp_concl;
       val raw_thm = (case find_first (fn thm =>
             Pattern.matches thy (Thm.concl_of thm, concl)) raw_thms of
           SOME thm => thm