--- 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