--- a/src/Pure/ML/ml_context.ML Sun Feb 16 21:33:28 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Mon Feb 17 11:14:26 2014 +0100
@@ -158,7 +158,7 @@
fun no_decl _ = ([], []);
fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
- | expand (Antiquote.Antiq (ss, range)) ctxt =
+ | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
let
val (decl, ctxt') = antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));