# HG changeset patch
# User blanchet
# Date 1444079030 -7200
# Node ID 20af2ad9261e85538e151569efdfcef0c8da8895
# Parent  426c9c85809927b49945f04f9239bdede2be80e8
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes

diff -r 426c9c858099 -r 20af2ad9261e src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Oct 05 21:46:48 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Oct 05 23:03:50 2015 +0200
@@ -79,7 +79,7 @@
         val fact_names = map fst used_facts
         val {facts = chained, goal, ...} = Proof.goal state
         val goal_t = Logic.get_goal (Thm.prop_of goal) i
-          |> add_chained (map Thm.prop_of chained)
+          |> add_chained (map (Thm.prop_of o forall_intr_vars) chained)
 
         fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
           | try_methss ress [] =
diff -r 426c9c858099 -r 20af2ad9261e src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Oct 05 21:46:48 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Oct 05 23:03:50 2015 +0200
@@ -117,7 +117,11 @@
   Method.insert_tac local_facts THEN'
   (case meth of
     Metis_Method (type_enc_opt, lam_trans_opt) =>
-    let val ctxt = Config.put Metis_Tactic.verbose false ctxt in
+    let
+      val ctxt = ctxt
+        |> Config.put Metis_Tactic.verbose false
+        |> Config.put Metis_Tactic.trace false
+    in
       Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
         (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
     end
diff -r 426c9c858099 -r 20af2ad9261e src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Oct 05 21:46:48 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Oct 05 23:03:50 2015 +0200
@@ -140,7 +140,10 @@
   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
 
 fun hackish_string_of_term ctxt =
-  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> YXML.content_of #> simplify_spaces
+  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
 
 val spying_version = "d"