--- a/src/Pure/ML/ml_context.ML Thu Aug 07 19:21:42 2008 +0200
+++ b/src/Pure/ML/ml_context.ML Thu Aug 07 19:21:43 2008 +0200
@@ -138,10 +138,10 @@
fun no_decl _ = ("", "");
fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state)
- | expand (Antiquote.Antiq (x, _)) (scope, background) =
+ | expand (Antiquote.Antiq x) (scope, background) =
let
val context = Stack.top scope;
- val (f, context') = antiquotation (Antiquote.read_arguments lex antiq x) context;
+ val (f, context') = antiquotation (Antiquote.read_antiq lex antiq x) context;
val (decl, background') = f {background = background, struct_name = struct_name};
in (decl, (Stack.map_top (K context') scope, background')) end
| expand (Antiquote.Open _) (scope, background) =