centralized term printing code

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 11:32:22 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 11:52:37 2012 +0100
@@ -231,12 +231,8 @@
     exists_low_level_class_const t orelse is_that_fact th
   end
 
-fun hackish_string_for_term ctxt t =
-  Print_Mode.setmp
-    (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
-    (Syntax.string_of_term ctxt) t
-  |> String.translate (fn c => if Char.isPrint c then str c else "")
-  |> simplify_spaces
+fun hackish_string_for_term ctxt =
+  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> repair_printed_term
 
 (* 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

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 12 11:32:22 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 12 11:52:37 2012 +0100
@@ -625,13 +625,11 @@
 
 fun string_for_proof ctxt type_enc lam_trans i n =
   let
-    fun fix_print_mode f x =
-      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
-                               (print_mode_value ())) f x
     fun do_indent ind = replicate_string (ind * indent_size) " "
     fun do_free (s, T) =
       maybe_quote s ^ " :: " ^
-      maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
+      maybe_quote (repair_printed_term (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 =
       (if member (op =) qs Moreover then "moreover " else "") ^
@@ -641,8 +639,10 @@
        else
          if member (op =) qs Show then "show" else "have")
     val do_term =
-      maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
-      o annotate_types ctxt
+      annotate_types ctxt
+      #> with_vanilla_print_mode (Syntax.string_of_term ctxt)
+      #> repair_printed_term
+      #> maybe_quote
     val reconstr = Metis (type_enc, lam_trans)
     fun do_facts ind (ls, ss) =
       "\n" ^ do_indent (ind + 1) ^
@@ -780,7 +780,7 @@
 
     (* proof references *)
     fun refs (Prove (_, _, _, By_Metis (refs, _))) =
-      map (the o Label_Table.lookup label_index_table) refs
+        map (the o Label_Table.lookup label_index_table) refs
       | refs _ = []
     val refed_by_vect =
       Vector.tabulate (n, (fn _ => []))
@@ -791,7 +791,6 @@
        algorithm) *)
     fun cost (Prove (_, _ , t, _)) = Term.size_of_term t
       | cost _ = 0
-    val cand_ord =  rev_order o prod_ord int_ord int_ord
     val cand_tab =
       v_fold_index
         (fn (i, [_]) => cons (get i proof_vect |> the |> cost, i)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Nov 12 11:32:22 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Nov 12 11:52:37 2012 +0100
@@ -18,6 +18,8 @@
   val subgoal_count : Proof.state -> int
   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 =
@@ -101,4 +103,12 @@
       [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
   in names end
 
+fun with_vanilla_print_mode f x =
+  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;