# 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