# HG changeset patch
# User blanchet
# Date 1352718416 -3600
# Node ID dd6a4655cd7211f7cdfca2f7a4212745d2280a8a
# Parent  fb024bbf4b656d2e0b3072ae5265b62ec11373ad
avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit

diff -r fb024bbf4b65 -r dd6a4655cd72 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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
diff -r fb024bbf4b65 -r dd6a4655cd72 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 12 11:52:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 12 12:06:56 2012 +0100
@@ -628,7 +628,7 @@
     fun do_indent ind = replicate_string (ind * indent_size) " "
     fun do_free (s, T) =
       maybe_quote s ^ " :: " ^
-      maybe_quote (repair_printed_term (with_vanilla_print_mode
+      maybe_quote (simplify_spaces (with_vanilla_print_mode
         (Syntax.string_of_typ ctxt) T))
     fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
     fun do_have qs =
@@ -641,7 +641,7 @@
     val do_term =
       annotate_types ctxt
       #> with_vanilla_print_mode (Syntax.string_of_term ctxt)
-      #> repair_printed_term
+      #> simplify_spaces
       #> maybe_quote
     val reconstr = Metis (type_enc, lam_trans)
     fun do_facts ind (ls, ss) =
diff -r fb024bbf4b65 -r dd6a4655cd72 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Nov 12 11:52:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Nov 12 12:06:56 2012 +0100
@@ -19,7 +19,6 @@
   val reserved_isar_keyword_table : unit -> unit Symtab.table
   val thms_in_proof : unit Symtab.table option -> thm -> string list
   val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
-  val repair_printed_term : string -> string
 end;
 
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -107,8 +106,4 @@
   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                            (print_mode_value ())) f x
 
-val repair_printed_term =
-  String.translate (fn c => if Char.isPrint c then str c else "")
-  #> simplify_spaces
-
 end;