src/Pure/ML/ml_context.ML
changeset 27781 5a82ee34e9fc
parent 27771 98499933a50f
child 27809 a1e409db516b
--- 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) =