--- 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) =>