Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed accidental '@{print}'
authorblanchet
Mon, 15 Sep 2014 12:30:06 +0200
changeset 58341 6c8b30b9f583
parent 58340 5f6f48e87de6
child 58342 9a82544fd29f
removed accidental '@{print}'
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle