# HG changeset patch
# User blanchet
# Date 1410777006 -7200
# Node ID 6c8b30b9f58310dc9b23e0c8b38bc68c7011b43d
# Parent  5f6f48e87de69e5983b773b29190e17975da4728
removed accidental '@{print}'

diff -r 5f6f48e87de6 -r 6c8b30b9f583 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Sep 15 12:11:41 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Sep 15 12:30:06 2014 +0200
@@ -168,7 +168,7 @@
           | SOME n => n)
 
         fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
-        fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev |> @{print}
+        fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
 
         fun get_role keep_role ((num, _), role, t, rule, _) =
           if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE