--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Jul 31 13:19:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 01 14:43:57 2014 +0200
@@ -142,9 +142,9 @@
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
fun hackish_string_of_term ctxt =
- with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
+ with_vanilla_print_mode (Syntax.string_of_term ctxt) #> unyxml #> simplify_spaces
-val spying_version = "c"
+val spying_version = "d"
fun spying false _ = ()
| spying true f =