--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Nov 12 11:52:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Nov 12 12:06:56 2012 +0100
@@ -232,7 +232,7 @@
end
fun hackish_string_for_term ctxt =
- with_vanilla_print_mode (Syntax.string_of_term ctxt) #> repair_printed_term
+ with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
(* This is a terrible hack. Free variables are sometimes coded as "M__" when
they are displayed as "M" and we want to avoid clashes with these. But