implicit "cartouche" method (experimental, undocumented);

--- a/src/HOL/ex/Cartouche_Examples.thy	Sun Jan 19 21:00:42 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sun Jan 19 21:33:45 2014 +0100
@@ -82,6 +82,9 @@
 end;
 *}
 
+
+subsection {* Explicit version: method with cartouche argument *}
+
 method_setup ml_tactic = {*
   Scan.lift Args.cartouche_source_position
     >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
@@ -100,4 +103,22 @@
 
 text {* @{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"} *}
 
+
+subsection {* Implicit version: method with special name "cartouche" (dynamic!) *}
+
+method_setup "cartouche" = {*
+  Scan.lift Args.cartouche_source_position
+    >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
+*}
+
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+  apply \<open>rtac @{thm impI} 1\<close>
+  apply \<open>etac @{thm conjE} 1\<close>
+  apply \<open>rtac @{thm conjI} 1\<close>
+  apply \<open>ALLGOALS atac\<close>
+  done
+
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+  by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+)
+
 end

--- a/src/Pure/Isar/method.ML	Sun Jan 19 21:00:42 2014 +0100
+++ b/src/Pure/Isar/method.ML	Sun Jan 19 21:33:45 2014 +0100
@@ -406,6 +406,9 @@
 
 fun meth4 x =
  (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
+  (* FIXME implicit "cartouche" method (experimental, undocumented) *)
+  Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
+    Source (Args.src (("cartouche", [tok]), Token.position_of tok))) ||
   Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
 and meth3 x =
  (meth4 --| Parse.$$$ "?" >> Try ||