# HG changeset patch
# User wenzelm
# Date 1464031830 -7200
# Node ID 629a4c5e953ed82a51f95170f6ab1b8be8c0d417
# Parent  547460dc5c1ef80babac9b255dd50e1e268f2de6
embedded content may be delimited via cartouches;

diff -r 547460dc5c1e -r 629a4c5e953e NEWS
--- a/NEWS	Mon May 23 20:45:10 2016 +0200
+++ b/NEWS	Mon May 23 21:30:30 2016 +0200
@@ -9,6 +9,10 @@
 
 *** General ***
 
+* Embedded content (e.g. the inner syntax of types, terms, props) may be
+delimited uniformly via cartouches. This works better than old-fashioned
+quotes when sub-languages are nested.
+
 * Type-inference improves sorts of newly introduced type variables for
 the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
 Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
diff -r 547460dc5c1e -r 629a4c5e953e src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/CCL/CCL.thy	Mon May 23 21:30:30 2016 +0200
@@ -474,7 +474,7 @@
   done
 
 method_setup eq_coinduct3 = \<open>
-  Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
+  Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
     SIMPLE_METHOD'
       (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3}))
 \<close>
diff -r 547460dc5c1e -r 629a4c5e953e src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/CCL/Wfd.thy	Mon May 23 21:30:30 2016 +0200
@@ -47,7 +47,7 @@
   done
 
 method_setup wfd_strengthen = \<open>
-  Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
+  Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
     SIMPLE_METHOD' (fn i =>
       Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] [] @{thm wfd_strengthen_lemma} i
         THEN assume_tac ctxt (i + 1)))
diff -r 547460dc5c1e -r 629a4c5e953e src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/CTT/CTT.thy	Mon May 23 21:30:30 2016 +0200
@@ -449,7 +449,7 @@
 
 method_setup eqintr = \<open>Scan.succeed (SIMPLE_METHOD o eqintr_tac)\<close>
 method_setup NE = \<open>
-  Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
+  Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
 \<close>
 method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close>
 method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close>
diff -r 547460dc5c1e -r 629a4c5e953e src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Mon May 23 21:30:30 2016 +0200
@@ -177,8 +177,8 @@
       @@{antiquotation const} options @{syntax term} |
       @@{antiquotation abbrev} options @{syntax term} |
       @@{antiquotation typ} options @{syntax type} |
-      @@{antiquotation type} options @{syntax name} |
-      @@{antiquotation class} options @{syntax name} |
+      @@{antiquotation type} options @{syntax embedded} |
+      @@{antiquotation class} options @{syntax embedded} |
       (@@{antiquotation command} | @@{antiquotation method} | @@{antiquotation attribute})
         options @{syntax name}
     ;
@@ -197,7 +197,7 @@
       @@{antiquotation verbatim} options @{syntax text} |
       @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation file_unchecked} options @{syntax name} |
-      @@{antiquotation url} options @{syntax name} |
+      @@{antiquotation url} options @{syntax embedded} |
       @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
     ;
     styles: '(' (style + ',') ')'
diff -r 547460dc5c1e -r 629a4c5e953e src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon May 23 21:30:30 2016 +0200
@@ -184,7 +184,7 @@
 
   @{rail \<open>
     @{syntax_def name}: @{syntax ident} | @{syntax longident} |
-      @{syntax symident} | @{syntax string} | @{syntax nat}
+      @{syntax symident} | @{syntax nat} | @{syntax string}
     ;
     @{syntax_def par_name}: '(' @{syntax name} ')'
   \<close>}
@@ -209,6 +209,24 @@
 \<close>
 
 
+subsection \<open>Embedded content\<close>
+
+text \<open>
+  Entity @{syntax embedded} refers to content of other languages: cartouches
+  allow arbitrary nesting of sub-languages that respect the recursive
+  balancing of cartouche delimiters. Quoted strings are possible as well, but
+  require escaped quotes when nested. As a shortcut, tokens that appear as
+  plain identifiers in the outer language may be used as inner language
+  content without delimiters.
+
+  @{rail \<open>
+    @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} |
+      @{syntax ident} | @{syntax longident} | @{syntax symident} |
+      @{syntax nat}
+  \<close>}
+\<close>
+
+
 subsection \<open>Comments \label{sec:comments}\<close>
 
 text \<open>
@@ -260,10 +278,10 @@
   as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
 
   @{rail \<open>
-    @{syntax_def type}: @{syntax name} | @{syntax typefree} |
+    @{syntax_def type}: @{syntax embedded} | @{syntax typefree} |
       @{syntax typevar}
     ;
-    @{syntax_def term}: @{syntax name} | @{syntax var}
+    @{syntax_def term}: @{syntax embedded} | @{syntax var}
     ;
     @{syntax_def prop}: @{syntax term}
   \<close>}
diff -r 547460dc5c1e -r 629a4c5e953e src/Doc/Prog_Prove/LaTeXsugar.thy
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy	Mon May 23 21:30:30 2016 +0200
@@ -52,7 +52,7 @@
       end
   in
     Thy_Output.antiquotation @{binding "const_typ"}
-     (Scan.lift Args.name_inner_syntax)
+     (Scan.lift Args.embedded_inner_syntax)
        (fn {source = src, context = ctxt, ...} => fn arg =>
           Thy_Output.output ctxt
             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
diff -r 547460dc5c1e -r 629a4c5e953e src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/FOL/FOL.thy	Mon May 23 21:30:30 2016 +0200
@@ -72,7 +72,7 @@
 \<close>
 
 method_setup case_tac = \<open>
-  Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
+  Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
     (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
 \<close> "case_tac emulation (dynamic instantiation!)"
 
diff -r 547460dc5c1e -r 629a4c5e953e src/HOL/Eisbach/parse_tools.ML
--- a/src/HOL/Eisbach/parse_tools.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/HOL/Eisbach/parse_tools.ML	Mon May 23 21:30:30 2016 +0200
@@ -34,7 +34,7 @@
     (fn ((_, SOME t), _) => Real_Val t
       | ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Term t)) tok)));
 
-val name_term = parse_term_val Args.name_inner_syntax;
+val name_term = parse_term_val Args.embedded_inner_syntax;
 
 fun is_real_val (Real_Val _) = true
   | is_real_val _ = false;
diff -r 547460dc5c1e -r 629a4c5e953e src/HOL/HOLCF/IOA/CompoScheds.thy
--- a/src/HOL/HOLCF/IOA/CompoScheds.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/HOL/HOLCF/IOA/CompoScheds.thy	Mon May 23 21:30:30 2016 +0200
@@ -289,7 +289,7 @@
 \<close>
 
 method_setup mkex_induct = \<open>
-  Scan.lift (Args.name -- Args.name -- Args.name)
+  Scan.lift (Args.embedded -- Args.embedded -- Args.embedded)
     >> (fn ((sch, exA), exB) => fn ctxt =>
       SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
 \<close>
diff -r 547460dc5c1e -r 629a4c5e953e src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Mon May 23 21:30:30 2016 +0200
@@ -996,13 +996,13 @@
 \<close>
 
 method_setup Seq_case =
-  \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
+  \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
 
 method_setup Seq_case_simp =
-  \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
+  \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
 
 method_setup Seq_induct =
-  \<open>Scan.lift Args.name --
+  \<open>Scan.lift Args.embedded --
     Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
     >> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (Seq_induct_tac ctxt s rws))\<close>
 
@@ -1010,10 +1010,10 @@
   \<open>Scan.succeed (SIMPLE_METHOD' o Seq_Finite_induct_tac)\<close>
 
 method_setup pair =
-  \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
+  \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
 
 method_setup pair_induct =
-  \<open>Scan.lift Args.name --
+  \<open>Scan.lift Args.embedded --
     Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
     >> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (pair_induct_tac ctxt s rws))\<close>
 
diff -r 547460dc5c1e -r 629a4c5e953e src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Mon May 23 21:30:30 2016 +0200
@@ -105,7 +105,7 @@
       end
   in
     Thy_Output.antiquotation @{binding "const_typ"}
-     (Scan.lift Args.name_inner_syntax)
+     (Scan.lift Args.embedded_inner_syntax)
        (fn {source = src, context = ctxt, ...} => fn arg =>
           Thy_Output.output ctxt
             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
diff -r 547460dc5c1e -r 629a4c5e953e src/HOL/Tools/functor.ML
--- a/src/HOL/Tools/functor.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/HOL/Tools/functor.ML	Mon May 23 21:30:30 2016 +0200
@@ -277,7 +277,6 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword functor}
     "register operations managing the functorial structure of a type"
-    (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
-      >> (fn (prfx, t) => functor_cmd prfx t));
+    (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term >> uncurry functor_cmd);
 
 end;
diff -r 547460dc5c1e -r 629a4c5e953e src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy	Mon May 23 21:30:30 2016 +0200
@@ -16,7 +16,7 @@
     "for proving safety properties"
 
 method_setup ensures_tac = {*
-  Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
+  Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
 *} "for proving progress properties"
 
diff -r 547460dc5c1e -r 629a4c5e953e src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Mon May 23 21:30:30 2016 +0200
@@ -7,7 +7,7 @@
 theory Cartouche_Examples
 imports Main
 keywords
-  "cartouche" "term_cartouche" :: diag and
+  "cartouche" :: diag and
   "text_cartouche" :: thy_decl
 begin
 
@@ -19,21 +19,23 @@
 
 notepad
 begin
-  txt \<open>Moreover, cartouches work as additional syntax in the
-    \<open>altstring\<close> category, for literal fact references.  For example:\<close>
+  txt \<open>Cartouches work as additional syntax for embedded language tokens
+    (types, terms, props) and as a replacement for the \<open>altstring\<close> category
+    (for literal fact references). For example:\<close>
 
   fix x y :: 'a
-  assume "x = y"
+  assume \<open>x = y\<close>
   note \<open>x = y\<close>
-  have "x = y" by (rule \<open>x = y\<close>)
-  from \<open>x = y\<close> have "x = y" .
+  have \<open>x = y\<close> by (rule \<open>x = y\<close>)
+  from \<open>x = y\<close> have \<open>x = y\<close> .
 
   txt \<open>Of course, this can be nested inside formal comments and
     antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
     [OF \<open>x = y\<close>]}.\<close>
 
-  have "x = y"
-    by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>)  \<comment> \<open>more cartouches involving ML\<close>
+  have \<open>x = y\<close>
+    by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>)
+      \<comment> \<open>more cartouches involving ML\<close>
 end
 
 
@@ -78,92 +80,55 @@
   end;
 \<close>
 
-syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string"  ("_")
+syntax "_cartouche_string" :: \<open>cartouche_position \<Rightarrow> string\<close>  ("_")
 
 parse_translation \<open>
   [(@{syntax_const "_cartouche_string"},
     K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
 \<close>
 
-term "\<open>\<close>"
-term "\<open>abc\<close>"
-term "\<open>abc\<close> @ \<open>xyz\<close>"
-term "\<open>\<newline>\<close>"
-term "\<open>\001\010\100\<close>"
+term \<open>\<open>\<close>\<close>
+term \<open>\<open>abc\<close>\<close>
+term \<open>\<open>abc\<close> @ \<open>xyz\<close>\<close>
+term \<open>\<open>\<newline>\<close>\<close>
 
 
 subsection \<open>Alternate outer and inner syntax: string literals\<close>
 
 subsubsection \<open>Nested quotes\<close>
 
-syntax "_string_string" :: "string_position \<Rightarrow> string"  ("_")
+syntax "_string_string" :: \<open>string_position \<Rightarrow> string\<close>  ("_")
 
 parse_translation \<open>
   [(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))]
 \<close>
 
-term "\"\""
-term "\"abc\""
-term "\"abc\" @ \"xyz\""
-term "\"\<newline>\""
-term "\"\001\010\100\""
-
-
-subsubsection \<open>Term cartouche and regular quotes\<close>
-
-ML \<open>
-  Outer_Syntax.command @{command_keyword term_cartouche} ""
-    (Parse.inner_syntax Parse.cartouche >> (fn s =>
-      Toplevel.keep (fn state =>
-        let
-          val ctxt = Toplevel.context_of state;
-          val t = Syntax.read_term ctxt s;
-        in writeln (Syntax.string_of_term ctxt t) end)))
-\<close>
-
-term_cartouche \<open>""\<close>
-term_cartouche \<open>"abc"\<close>
-term_cartouche \<open>"abc" @ "xyz"\<close>
-term_cartouche \<open>"\<newline>"\<close>
-term_cartouche \<open>"\001\010\100"\<close>
+term \<open>""\<close>
+term \<open>"abc"\<close>
+term \<open>"abc" @ "xyz"\<close>
+term \<open>"\<newline>"\<close>
+term \<open>"\001\010\100"\<close>
 
 
 subsubsection \<open>Further nesting: antiquotations\<close>
 
-setup \<comment> "ML antiquotation"
-\<open>
-  ML_Antiquotation.inline @{binding term_cartouche}
-    (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >>
-      (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s))))
-\<close>
-
-setup \<comment> "document antiquotation"
-\<open>
-  Thy_Output.antiquotation @{binding ML_cartouche}
-    (Scan.lift Args.cartouche_input) (fn {context, ...} => fn source =>
-      let
-        val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");";
-        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
-      in "" end);
-\<close>
-
 ML \<open>
-  @{term_cartouche \<open>""\<close>};
-  @{term_cartouche \<open>"abc"\<close>};
-  @{term_cartouche \<open>"abc" @ "xyz"\<close>};
-  @{term_cartouche \<open>"\<newline>"\<close>};
-  @{term_cartouche \<open>"\001\010\100"\<close>};
+  @{term \<open>""\<close>};
+  @{term \<open>"abc"\<close>};
+  @{term \<open>"abc" @ "xyz"\<close>};
+  @{term \<open>"\<newline>"\<close>};
+  @{term \<open>"\001\010\100"\<close>};
 \<close>
 
 text \<open>
-  @{ML_cartouche
+  @{ML
     \<open>
       (
-        @{term_cartouche \<open>""\<close>};
-        @{term_cartouche \<open>"abc"\<close>};
-        @{term_cartouche \<open>"abc" @ "xyz"\<close>};
-        @{term_cartouche \<open>"\<newline>"\<close>};
-        @{term_cartouche \<open>"\001\010\100"\<close>}
+        @{term \<open>""\<close>};
+        @{term \<open>"abc"\<close>};
+        @{term \<open>"abc" @ "xyz"\<close>};
+        @{term \<open>"\<newline>"\<close>};
+        @{term \<open>"\001\010\100"\<close>}
       )
     \<close>
   }
@@ -181,14 +146,14 @@
 
 text_cartouche
 \<open>
-  @{ML_cartouche
+  @{ML
     \<open>
       (
-        @{term_cartouche \<open>""\<close>};
-        @{term_cartouche \<open>"abc"\<close>};
-        @{term_cartouche \<open>"abc" @ "xyz"\<close>};
-        @{term_cartouche \<open>"\<newline>"\<close>};
-        @{term_cartouche \<open>"\001\010\100"\<close>}
+        @{term \<open>""\<close>};
+        @{term \<open>"abc"\<close>};
+        @{term \<open>"abc" @ "xyz"\<close>};
+        @{term \<open>"\<newline>"\<close>};
+        @{term \<open>"\001\010\100"\<close>}
       )
     \<close>
   }
@@ -226,18 +191,18 @@
     >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
 \<close>
 
-lemma "A \<and> B \<longrightarrow> B \<and> A"
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
   apply (ml_tactic \<open>resolve_tac @{context} @{thms impI} 1\<close>)
   apply (ml_tactic \<open>eresolve_tac @{context} @{thms conjE} 1\<close>)
   apply (ml_tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>)
   apply (ml_tactic \<open>ALLGOALS (assume_tac @{context})\<close>)
   done
 
-lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)
 
-ML \<open>@{lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>
+ML \<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>
 
-text \<open>@{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"}\<close>
+text \<open>@{ML \<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>}\<close>
 
 
 subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close>
@@ -247,14 +212,14 @@
     >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
 \<close>
 
-lemma "A \<and> B \<longrightarrow> B \<and> A"
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
   apply \<open>resolve_tac @{context} @{thms impI} 1\<close>
   apply \<open>eresolve_tac @{context} @{thms conjE} 1\<close>
   apply \<open>resolve_tac @{context} @{thms conjI} 1\<close>
   apply \<open>ALLGOALS (assume_tac @{context})\<close>
   done
 
-lemma "A \<and> B \<longrightarrow> B \<and> A"
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
   by (\<open>resolve_tac @{context} @{thms impI} 1\<close>,
     \<open>eresolve_tac @{context} @{thms conjE} 1\<close>,
     \<open>resolve_tac @{context} @{thms conjI} 1\<close>,
diff -r 547460dc5c1e -r 629a4c5e953e src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/LCF/LCF.thy	Mon May 23 21:30:30 2016 +0200
@@ -319,7 +319,7 @@
   adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
 
 method_setup induct = \<open>
-  Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt =>
+  Scan.lift Args.embedded_inner_syntax >> (fn v => fn ctxt =>
     SIMPLE_METHOD' (fn i =>
       Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] [] @{thm induct} i THEN
       REPEAT (resolve_tac ctxt @{thms adm_lemmas} i)))
diff -r 547460dc5c1e -r 629a4c5e953e src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/Pure/Isar/args.ML	Mon May 23 21:30:30 2016 +0200
@@ -23,12 +23,14 @@
   val mode: string -> bool parser
   val maybe: 'a parser -> 'a option parser
   val name_token: Token.T parser
-  val name_inner_syntax: string parser
-  val name_input: Input.source parser
   val name: string parser
   val cartouche_inner_syntax: string parser
   val cartouche_input: Input.source parser
   val text_token: Token.T parser
+  val embedded_token: Token.T parser
+  val embedded_inner_syntax: string parser
+  val embedded_input: Input.source parser
+  val embedded: string parser
   val text_input: Input.source parser
   val text: string parser
   val binding: binding parser
@@ -104,15 +106,18 @@
 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
 
 val name_token = ident || string;
-val name_inner_syntax = name_token >> Token.inner_syntax_of;
-val name_input = name_token >> Token.input_of;
 val name = name_token >> Token.content_of;
 
 val cartouche = Parse.token Parse.cartouche;
 val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
 val cartouche_input = cartouche >> Token.input_of;
 
-val text_token = name_token || Parse.token (Parse.verbatim || Parse.cartouche);
+val embedded_token = ident || string || cartouche;
+val embedded_inner_syntax = embedded_token >> Token.inner_syntax_of;
+val embedded_input = embedded_token >> Token.input_of;
+val embedded = embedded_token >> Token.content_of;
+
+val text_token = embedded_token || Parse.token Parse.verbatim;
 val text_input = text_token >> Token.input_of;
 val text = text_token >> Token.content_of;
 
@@ -120,8 +125,9 @@
 val alt_name = alt_string >> Token.content_of;
 val liberal_name = (symbolic >> Token.content_of) || name;
 
-val var = (ident >> Token.content_of) :|-- (fn x =>
-  (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
+val var =
+  (ident >> Token.content_of) :|-- (fn x =>
+    (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
 
 
 (* values *)
@@ -141,10 +147,10 @@
   internal_source || name_token >> Token.evaluate Token.Source read;
 
 fun named_typ read =
-  internal_typ || name_token >> Token.evaluate Token.Typ (read o Token.inner_syntax_of);
+  internal_typ || embedded_token >> Token.evaluate Token.Typ (read o Token.inner_syntax_of);
 
 fun named_term read =
-  internal_term || name_token >> Token.evaluate Token.Term (read o Token.inner_syntax_of);
+  internal_term || embedded_token >> Token.evaluate Token.Term (read o Token.inner_syntax_of);
 
 fun named_fact get =
   internal_fact ||
diff -r 547460dc5c1e -r 629a4c5e953e src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Mon May 23 21:30:30 2016 +0200
@@ -62,8 +62,9 @@
   val list: 'a parser -> 'a list parser
   val list1: 'a parser -> 'a list parser
   val properties: Properties.T parser
-  val name: bstring parser
+  val name: string parser
   val binding: binding parser
+  val embedded: string parser
   val text: string parser
   val path: string parser
   val theory_name: string parser
@@ -257,16 +258,21 @@
 val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")");
 
 
-(* names and text *)
+(* names and embedded content *)
 
 val name =
-  group (fn () => "name") (short_ident || long_ident || sym_ident || string || number);
+  group (fn () => "name")
+    (short_ident || long_ident || sym_ident || number || string);
 
 val binding = position name >> Binding.make;
 
+val embedded =
+  group (fn () => "embedded content")
+    (short_ident || long_ident || sym_ident || number || string || cartouche);
+
 val text =
   group (fn () => "text")
-    (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
+    (short_ident || long_ident || sym_ident || number || string || verbatim || cartouche);
 
 val path = group (fn () => "file name/path specification") name;
 
@@ -280,11 +286,11 @@
 
 (* type classes *)
 
-val class = group (fn () => "type class") (inner_syntax name);
+val class = group (fn () => "type class") (inner_syntax embedded);
 
-val sort = group (fn () => "sort") (inner_syntax name);
+val sort = group (fn () => "sort") (inner_syntax embedded);
 
-val type_const = inner_syntax (group (fn () => "type constructor") name);
+val type_const = group (fn () => "type constructor") (inner_syntax embedded);
 
 val arity = type_const -- ($$$ "::" |-- !!!
   (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2;
@@ -297,7 +303,8 @@
 
 val typ_group =
   group (fn () => "type")
-    (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
+    (short_ident || long_ident || sym_ident || type_ident || type_var || number ||
+      string || cartouche);
 
 val typ = inner_syntax typ_group;
 
@@ -386,15 +393,13 @@
 
 (* terms *)
 
-val tm = short_ident || long_ident || sym_ident || term_var || number || string;
-
-val term_group = group (fn () => "term") tm;
-val prop_group = group (fn () => "proposition") tm;
+val term_group = group (fn () => "term") (term_var || embedded);
+val prop_group = group (fn () => "proposition") (term_var || embedded);
 
 val term = inner_syntax term_group;
 val prop = inner_syntax prop_group;
 
-val const = inner_syntax (group (fn () => "constant") name);
+val const = group (fn () => "constant") (inner_syntax embedded);
 
 val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
 
diff -r 547460dc5c1e -r 629a4c5e953e src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Mon May 23 21:30:30 2016 +0200
@@ -17,7 +17,7 @@
     (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
 
   ML_Antiquotation.declaration @{binding print}
-    (Scan.lift (Scan.optional Args.name "Output.writeln"))
+    (Scan.lift (Scan.optional Args.embedded "Output.writeln"))
       (fn src => fn output => fn ctxt =>
         let
           val struct_name = ML_Context.struct_name ctxt;
@@ -86,7 +86,7 @@
 
 (* type classes *)
 
-fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
+fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
   Proof_Context.read_class ctxt s
   |> syn ? Lexicon.mark_class
   |> ML_Syntax.print_string);
@@ -96,13 +96,13 @@
   ML_Antiquotation.inline @{binding class_syntax} (class true) #>
 
   ML_Antiquotation.inline @{binding sort}
-    (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
+    (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
       ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
 
 
 (* type constructors *)
 
-fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
+fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
       val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
@@ -126,7 +126,7 @@
 
 (* constants *)
 
-fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
+fun const_name check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
       val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
@@ -143,13 +143,13 @@
     (const_name (fn (_, c) => Lexicon.mark_const c)) #>
 
   ML_Antiquotation.inline @{binding syntax_const}
-    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
+    (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (c, pos)) =>
       if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
       then ML_Syntax.print_string c
       else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
 
   ML_Antiquotation.inline @{binding const}
-    (Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) -- Scan.optional
+    (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional
         (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
       >> (fn ((ctxt, (raw_c, pos)), Ts) =>
         let
diff -r 547460dc5c1e -r 629a4c5e953e src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/Pure/ML/ml_thms.ML	Mon May 23 21:30:30 2016 +0200
@@ -77,7 +77,7 @@
 
 val and_ = Args.$$$ "and";
 val by = Parse.reserved "by";
-val goal = Scan.unless (by || and_) Args.name_inner_syntax;
+val goal = Scan.unless (by || and_) Args.embedded_inner_syntax;
 
 val _ = Theory.setup
   (ML_Antiquotation.declaration @{binding lemma}
diff -r 547460dc5c1e -r 629a4c5e953e src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Mon May 23 21:30:30 2016 +0200
@@ -195,7 +195,7 @@
 (* URLs *)
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
+  (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.embedded))
     (fn {context = ctxt, ...} => fn (name, pos) =>
       (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
        enclose "\\url{" "}" name)));
diff -r 547460dc5c1e -r 629a4c5e953e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon May 23 21:30:30 2016 +0200
@@ -645,10 +645,10 @@
   basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #>
   basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #>
   basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
-  basic_entity @{binding abbrev} (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
+  basic_entity @{binding abbrev} (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
   basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
-  basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
-  basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
+  basic_entity @{binding class} (Scan.lift Args.embedded_inner_syntax) pretty_class #>
+  basic_entity @{binding type} (Scan.lift Args.embedded) pretty_type #>
   basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
   basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
   basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
diff -r 547460dc5c1e -r 629a4c5e953e src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Mon May 23 21:30:30 2016 +0200
@@ -177,7 +177,8 @@
 (* where: named instantiation *)
 
 val named_insts =
-  Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax))
+  Parse.and_list1
+    (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.embedded_inner_syntax))
     -- Parse.for_fixes;
 
 val _ = Theory.setup
@@ -191,7 +192,7 @@
 
 local
 
-val inst = Args.maybe Args.name_inner_syntax;
+val inst = Args.maybe Args.embedded_inner_syntax;
 val concl = Args.$$$ "concl" -- Args.colon;
 
 val insts =
@@ -330,12 +331,12 @@
   Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
     "cut rule (dynamic instantiation)" #>
   Method.setup @{binding subgoal_tac}
-    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax -- Parse.for_fixes) >>
+    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >>
       (fn (quant, (props, fixes)) => fn ctxt =>
         SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props))))
     "insert subgoal (dynamic instantiation)" #>
   Method.setup @{binding thin_tac}
-    (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
+    (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
       (fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes)))
     "remove premise (dynamic instantiation)");
 
diff -r 547460dc5c1e -r 629a4c5e953e src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/Tools/induct_tacs.ML	Mon May 23 21:30:30 2016 +0200
@@ -122,14 +122,14 @@
 
 val varss =
   Parse.and_list'
-    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_inner_syntax))));
+    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.embedded_inner_syntax))));
 
 in
 
 val _ =
   Theory.setup
    (Method.setup @{binding case_tac}
-      (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) -- opt_rule >>
+      (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) -- opt_rule >>
         (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s xs r)))
       "unstructured case analysis on types" #>
     Method.setup @{binding induct_tac}
diff -r 547460dc5c1e -r 629a4c5e953e src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Mon May 23 21:30:30 2016 +0200
@@ -64,7 +64,7 @@
 val _ =
   Theory.setup
     (Method.setup @{binding "ind_cases"}
-      (Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
+      (Scan.lift (Scan.repeat1 Args.embedded_inner_syntax) >>
         (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
       "dynamic case analysis on sets");
 
diff -r 547460dc5c1e -r 629a4c5e953e src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Mon May 23 20:45:10 2016 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Mon May 23 21:30:30 2016 +0200
@@ -179,11 +179,11 @@
 val _ =
   Theory.setup
     (Method.setup @{binding induct_tac}
-      (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
+      (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >>
         (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s xs)))
       "induct_tac emulation (dynamic instantiation!)" #>
     Method.setup @{binding case_tac}
-     (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
+     (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >>
         (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s xs)))
       "datatype case_tac emulation (dynamic instantiation!)");
 
diff -r 547460dc5c1e -r 629a4c5e953e src/ZF/UNITY/SubstAx.thy
--- a/src/ZF/UNITY/SubstAx.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/ZF/UNITY/SubstAx.thy	Mon May 23 21:30:30 2016 +0200
@@ -373,7 +373,7 @@
 \<close>
 
 method_setup ensures = \<open>
-    Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
+    Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
     (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
 \<close> "for proving progress properties"