# HG changeset patch
# User blanchet
# Date 1285571679 -7200
# Node ID 6e8c231876f59c830fc1b5833f66f85beaea30ed
# Parent  d3f46f1ca1f1adae0bf0850c03695e9897a10987
remove needless flag

diff -r d3f46f1ca1f1 -r 6e8c231876f5 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Sep 27 08:47:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Sep 27 09:14:39 2010 +0200
@@ -740,8 +740,7 @@
           let
             val multi = length ths > 1
             fun backquotify th =
-              "`" ^ Print_Mode.setmp (Print_Mode.input ::
-                                      filter (curry (op =) Symbol.xsymbolsN)
+              "`" ^ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                                              (print_mode_value ()))
                    (Syntax.string_of_term ctxt) (close_form (prop_of th)) ^ "`"
               |> String.translate (fn c => if Char.isPrint c then str c else "")