--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Oct 05 21:46:48 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Oct 05 23:03:50 2015 +0200
@@ -140,7 +140,10 @@
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) #> YXML.content_of #> simplify_spaces
+ map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
+ #> with_vanilla_print_mode (Syntax.string_of_term ctxt)
+ #> YXML.content_of
+ #> simplify_spaces
val spying_version = "d"