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