# HG changeset patch
# User wenzelm
# Date 1546697721 -3600
# Node ID ec135235fbcc96e46dc724c68e763f339bb182ba
# Parent  1d340f7f8dce0e41afe763e7d1ae5f35219a8318
mark for isabelle update -u control_cartouches;

diff -r 1d340f7f8dce -r ec135235fbcc src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sat Jan 05 14:50:36 2019 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Sat Jan 05 15:15:21 2019 +0100
@@ -160,7 +160,7 @@
       then ML_Syntax.print_string c
       else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
 
-  ML_Antiquotation.inline \<^binding>\<open>const\<close>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>const\<close>
     (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) =>