# HG changeset patch
# User blanchet
# Date 1412083081 -7200
# Node ID 094efe6ac459623a6b7dc662a032a07cb312fb37
# Parent  59bdd4f5725583f2dfd35869d1d663b3f530d71d
don't affect other subgoals with 'auto' in one-liner proofs

diff -r 59bdd4f57255 -r 094efe6ac459 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Sep 30 14:54:14 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Sep 30 15:18:01 2014 +0200
@@ -80,6 +80,9 @@
   | is_proof_method_direct Simp_Size_Method = true
   | is_proof_method_direct _ = false
 
+fun is_proof_method_multi_goal Auto_Method = true
+  | is_proof_method_multi_goal _ = false
+
 fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
 
 fun string_of_proof_method ctxt ss meth =
@@ -163,7 +166,8 @@
 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
     (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
-    apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth
+    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 "")
   end
 
 fun try_command_line banner play command =