merged

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 12:27:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 12:28:19 2012 +0100
@@ -23,7 +23,7 @@
   val fact_from_ref :
     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
-  val backquote_thm : thm -> string
+  val backquote_thm : Proof.context -> thm -> string
   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
   val maybe_instantiate_inducts :
     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
@@ -231,12 +231,8 @@
     exists_low_level_class_const t orelse is_that_fact th
   end
 
-fun hackish_string_for_term thy t =
-  Print_Mode.setmp
-    (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
-    (Syntax.string_of_term_global thy) 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) #> 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
@@ -259,12 +255,12 @@
           (Term.add_vars t [] |> sort_wrt (fst o fst))
   |> fst
 
-fun backquote_term thy t =
+fun backquote_term ctxt t =
   t |> close_form
-    |> hackish_string_for_term thy
+    |> hackish_string_for_term ctxt
     |> backquote
 
-fun backquote_thm th = backquote_term (theory_of_thm th) (prop_of th)
+fun backquote_thm ctxt th = backquote_term ctxt (prop_of th)
 
 fun clasimpset_rule_table_of ctxt =
   let
@@ -328,14 +324,13 @@
 
 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
   let
-    val thy = Proof_Context.theory_of ctxt
     fun varify_noninducts (t as Free (s, T)) =
         if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
       | varify_noninducts t = t
     val p_inst =
       concl_prop |> map_aterms varify_noninducts |> close_form
                  |> lambda (Free ind_x)
-                 |> hackish_string_for_term thy
+                 |> hackish_string_for_term ctxt
   in
     ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
       stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
@@ -417,7 +412,7 @@
                              val new =
                                (((fn () =>
                                      if name0 = "" then
-                                       backquote_thm th
+                                       backquote_thm ctxt th
                                      else
                                        [Facts.extern ctxt facts name0,
                                         Name_Space.extern ctxt full_space name0]

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Nov 12 12:27:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Nov 12 12:28:19 2012 +0100
@@ -188,7 +188,7 @@
       | NONE => hint
     end
   else
-    backquote_thm th
+    backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th
 
 fun suggested_facts suggs facts =
   let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 12 12:27:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 12 12:28:19 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 (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 =
       (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)
+      #> simplify_spaces
+      #> 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 12:27:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Nov 12 12:28:19 2012 +0100
@@ -18,6 +18,7 @@
   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
 end;
 
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -101,4 +102,8 @@
       [] |> 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
+
 end;