# HG changeset patch
# User wenzelm
# Date 1638703390 -3600
# Node ID 89c7f74b5ae118f978bb5b07d5ae2c7ba9735867
# Parent  0263787a06b4fb34b30678db9d330db9727de219
clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);

diff -r 0263787a06b4 -r 89c7f74b5ae1 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sat Dec 04 20:30:16 2021 +0000
+++ b/src/Pure/Isar/parse.ML	Sun Dec 05 12:23:10 2021 +0100
@@ -120,7 +120,6 @@
   val thms1: (Facts.ref * Token.src list) list parser
   val options: ((string * Position.T) * (string * Position.T)) list parser
   val embedded_ml: ML_Lex.token Antiquote.antiquote list parser
-  val embedded_ml_underscore: ML_Lex.token Antiquote.antiquote list parser
   val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
   val read_embedded: Proof.context -> Keyword.keywords -> 'a parser -> Input.source -> 'a
   val read_embedded_src: Proof.context -> Keyword.keywords -> 'a parser -> Token.src -> 'a
@@ -505,12 +504,10 @@
 (* embedded ML *)
 
 val embedded_ml =
+  input underscore >> ML_Lex.read_source ||
   embedded_input >> ML_Lex.read_source ||
   control >> (ML_Lex.read_symbols o Antiquote.control_symbols);
 
-val embedded_ml_underscore =
-  input underscore >> ML_Lex.read_source || embedded_ml;
-
 
 (* read embedded source, e.g. for antiquotations *)
 
diff -r 0263787a06b4 -r 89c7f74b5ae1 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sat Dec 04 20:30:16 2021 +0000
+++ b/src/Pure/ML/ml_antiquotations.ML	Sun Dec 05 12:23:10 2021 +0100
@@ -207,7 +207,7 @@
 
 val parse_name = Parse.input Parse.name;
 
-val parse_args = Scan.repeat Parse.embedded_ml_underscore;
+val parse_args = Scan.repeat Parse.embedded_ml;
 val parse_for_args = Scan.optional (Parse.$$$ "for" |-- Parse.!!! parse_args) [];
 
 fun parse_body b =