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