# HG changeset patch
# User blanchet
# Date 1444905591 -7200
# Node ID 1502f2410d8bd028b2e7217f0929220f4497978d
# Parent  f6e314c1e9c4e6eee51d7cecaf70814291165d4b
removed too aggressive underscorization

diff -r f6e314c1e9c4 -r 1502f2410d8b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Oct 13 19:25:22 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Oct 15 12:39:51 2015 +0200
@@ -140,8 +140,8 @@
   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
 
 fun hackish_string_of_term ctxt =
-  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)
+  (* FIXME: 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