src/Pure/ML/ml_context.ML
changeset 58903 38c72f5f6c2e
parent 58011 bc6bced136e5
child 58928 23d0ffd48006
--- a/src/Pure/ML/ml_context.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -116,14 +116,14 @@
       then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
       else
         let
-          val lex = #1 (Keyword.get_lexicons ());
+          val keywords = Keyword.get_keywords ();
           fun no_decl _ = ([], []);
 
           fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
             | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
                 let
                   val (decl, ctxt') =
-                    apply_antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
+                    apply_antiquotation (Token.read_antiq keywords antiq (ss, #1 range)) ctxt;
                   val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
                 in (decl', ctxt') end;