1.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 09 17:54:09 2014 +0200
     1.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 09 20:58:32 2014 +0200
     1.3 @@ -27,6 +27,9 @@
     1.4    txt \<open>Of course, this can be nested inside formal comments and
     1.5      antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
     1.6      [OF \<open>x = y\<close>]}.\<close>
     1.7 +
     1.8 +  have "x = y"
     1.9 +    by (tactic \<open>rtac @{thm \<open>x = y\<close>} 1\<close>)  -- \<open>more cartouches involving ML\<close>
    1.10  end
    1.11  
    1.12  

     2.1 --- a/src/Pure/Isar/args.ML	Wed Apr 09 17:54:09 2014 +0200
     2.2 +++ b/src/Pure/Isar/args.ML	Wed Apr 09 20:58:32 2014 +0200
     2.3 @@ -33,6 +33,8 @@
     2.4    val maybe: 'a parser -> 'a option parser
     2.5    val cartouche_inner_syntax: string parser
     2.6    val cartouche_source_position: Symbol_Pos.source parser
     2.7 +  val text_source_position: Symbol_Pos.source parser
     2.8 +  val text: string parser
     2.9    val name_inner_syntax: string parser
    2.10    val name_source_position: Symbol_Pos.source parser
    2.11    val name: string parser
    2.12 @@ -151,7 +153,7 @@
    2.13    (Parse.short_ident || Parse.long_ident || Parse.sym_ident || Parse.term_var ||
    2.14      Parse.type_ident || Parse.type_var || Parse.number);
    2.15  
    2.16 -val string = Parse.token (Parse.string || Parse.verbatim);
    2.17 +val string = Parse.token Parse.string;
    2.18  val alt_string = Parse.token (Parse.alt_string || Parse.cartouche);
    2.19  val symbolic = Parse.token (Parse.keyword_with Token.ident_or_symbolic);
    2.20  
    2.21 @@ -163,7 +165,6 @@
    2.22        else Scan.fail
    2.23      end);
    2.24  
    2.25 -
    2.26  val named = ident || string;
    2.27  
    2.28  val add = $$$ "add";
    2.29 @@ -183,6 +184,10 @@
    2.30  val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
    2.31  val cartouche_source_position = cartouche >> Token.source_position_of;
    2.32  
    2.33 +val text_token = named || Parse.token (Parse.verbatim || Parse.cartouche);
    2.34 +val text_source_position = text_token >> Token.source_position_of;
    2.35 +val text = text_token >> Token.content_of;
    2.36 +
    2.37  val name_inner_syntax = named >> Token.inner_syntax_of;
    2.38  val name_source_position = named >> Token.source_position_of;
    2.39  

     3.1 --- a/src/Pure/Isar/method.ML	Wed Apr 09 17:54:09 2014 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Wed Apr 09 20:58:32 2014 +0200
     3.3 @@ -513,9 +513,9 @@
     3.4    setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
     3.5      (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
     3.6        "rotate assumptions of goal" #>
     3.7 -  setup @{binding tactic} (Scan.lift Args.name_source_position >> tactic)
     3.8 +  setup @{binding tactic} (Scan.lift Args.text_source_position >> tactic)
     3.9      "ML tactic as proof method" #>
    3.10 -  setup @{binding raw_tactic} (Scan.lift Args.name_source_position >> raw_tactic)
    3.11 +  setup @{binding raw_tactic} (Scan.lift Args.text_source_position >> raw_tactic)
    3.12      "ML tactic as raw proof method");
    3.13  
    3.14