src/Pure/ML/ml_antiquote.ML

--- a/src/Pure/ML/ml_antiquote.ML	Thu Aug 14 21:06:07 2008 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Fri Aug 15 15:50:44 2008 +0200
@@ -78,7 +78,7 @@
 
 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
 
-val _ = inline "sort" (Args.context -- Scan.lift Args.name >> (fn (ctxt, s) =>
+val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
   ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
 
 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
@@ -86,7 +86,7 @@
 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
 
 val _ = macro "let" (Args.context --
-  Scan.lift (P.and_list1 (P.and_list1 Args.name -- (Args.$$$ "=" |-- Args.name)))
+  Scan.lift (P.and_list1 (P.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
     >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
 
 val _ = macro "note" (Args.context :|-- (fn ctxt =>
@@ -104,11 +104,11 @@
   "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
 
 val _ = value "cpat"
-  (Args.context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
+  (Args.context -- Scan.lift Args.name_source >> uncurry ProofContext.read_term_pattern >> (fn t =>
     "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
 
 
-fun type_ syn = (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
+fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
     #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
     |> syn ? Sign.base_name
     |> ML_Syntax.print_string));
@@ -117,7 +117,7 @@
 val _ = inline "type_syntax" (type_ true);
 
 
-fun const syn = Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
+fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
   #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
   |> syn ? ProofContext.const_syntax_name ctxt
   |> ML_Syntax.print_string);
@@ -126,7 +126,7 @@
 val _ = inline "const_syntax" (const true);
 
 val _ = inline "const"
-  (Args.context -- Scan.lift Args.name -- Scan.optional
+  (Args.context -- Scan.lift Args.name_source -- Scan.optional
       (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
     >> (fn ((ctxt, c), Ts) =>
       let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)