# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID 02a53c1bbb6ca013ae6572b6db19752596fe214e
# Parent  18b8a8f1031343a5438a1d92332ea8937715d79e
generate backquotes without markup, since this confuses preplay; bump up spying version identifier;

diff -r 18b8a8f10313 -r 02a53c1bbb6c src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 31 13:19:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -77,8 +77,7 @@
   | explode_interval max (Facts.From i) = i upto i + max - 1
   | explode_interval _ (Facts.Single i) = [i]
 
-val backquote =
-  raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
+val backquote = raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
 
 (* unfolding these can yield really huge terms *)
 val risky_defs = @{thms Bit0_def Bit1_def}
diff -r 18b8a8f10313 -r 02a53c1bbb6c src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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 =