# HG changeset patch
# User blanchet
# Date 1430684129 -7200
# Node ID 2c468c06258981cd53dbbe4fcd668cc312fcaa90
# Parent  98754695b421f328baa4276c29b1dfd0bd0cd6c9
improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')

diff -r 98754695b421 -r 2c468c062589 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun May 03 18:14:11 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun May 03 22:15:29 2015 +0200
@@ -55,6 +55,8 @@
    del : (Facts.ref * Token.src list) list,
    only : bool}
 
+val local_thisN = Long_Name.localN ^ Long_Name.separator ^ Auto_Bind.thisN
+
 (* gracefully handle huge background theories *)
 val max_facts_for_duplicates = 50000
 val max_facts_for_complex_check = 25000
@@ -499,7 +501,7 @@
                else
                  let
                    fun get_name () =
-                     if name0 = "" then
+                     if name0 = "" orelse name0 = local_thisN then
                        backquote_thm ctxt th
                      else
                        let val short_name = Facts.extern ctxt facts name0 in
diff -r 98754695b421 -r 2c468c062589 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 03 18:14:11 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 03 22:15:29 2015 +0200
@@ -34,6 +34,7 @@
     ((string * stature) list * (proof_method * play_outcome)) * string * int * int
 
   val is_proof_method_direct : proof_method -> bool
+  val proof_method_distinguishes_chained_and_direct : proof_method -> bool
   val string_of_proof_method : Proof.context -> string list -> proof_method -> string
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
   val thms_influence_proof_method : Proof.context -> proof_method -> thm list -> bool
@@ -80,6 +81,10 @@
   | is_proof_method_direct Simp_Size_Method = true
   | is_proof_method_direct _ = false
 
+fun proof_method_distinguishes_chained_and_direct Simp_Method = true
+  | proof_method_distinguishes_chained_and_direct Simp_Size_Method = true
+  | proof_method_distinguishes_chained_and_direct _ = false
+
 fun is_proof_method_multi_goal Auto_Method = true
   | is_proof_method_multi_goal _ = false
 
@@ -163,8 +168,14 @@
   | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
 
 (* FIXME *)
-fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss =
-  let val (indirect_ss, direct_ss) = if is_proof_method_direct meth then ([], ss) else (ss, []) in
+fun proof_method_command ctxt meth i n used_chaineds _(*num_chained*) extras =
+  let
+    val (indirect_ss, direct_ss) =
+      if is_proof_method_direct meth then
+        ([], extras |> proof_method_distinguishes_chained_and_direct meth ? append used_chaineds)
+      else
+        (extras, [])
+  in
     (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
     apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth ^
     (if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "")