# HG changeset patch
# User wenzelm
# Date 1214408319 -7200
# Node ID 54b5367a827ab0478534c2e58b6366407a8e5263
# Parent  d6679949a869d356269c0eecc1f3f61f752723b0
re-use official outer keywords;

diff -r d6679949a869 -r 54b5367a827a src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Wed Jun 25 17:38:38 2008 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Jun 25 17:38:39 2008 +0200
@@ -122,8 +122,6 @@
 
 (* abstract fact values *)
 
-val _ = ML_Context.add_keywords ["[", "]", "(", ")", "-", ","];   (* FIXME !? *)
-
 structure AuxFacts = ProofDataFun
 (
   type T = thm list Inttab.table;
diff -r d6679949a869 -r 54b5367a827a src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Jun 25 17:38:38 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Wed Jun 25 17:38:39 2008 +0200
@@ -23,7 +23,6 @@
   val stored_thms: thm list ref
   val ml_store_thm: string * thm -> unit
   val ml_store_thms: string * thm list -> unit
-  val add_keywords: string list -> unit
   type antiq =
     {struct_name: string, background: Proof.context} ->
       (Proof.context -> string * string) * Proof.context
@@ -82,22 +81,6 @@
 
 (** ML antiquotations **)
 
-(* antiquotation keywords *)
-
-local
-
-val global_lexicon = ref Scan.empty_lexicon;
-
-in
-
-fun add_keywords keywords = CRITICAL (fn () =>
-  change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords)));
-
-fun get_lexicon () = ! global_lexicon;
-
-end;
-
-
 (* antiquotation commands *)
 
 type antiq =
@@ -150,7 +133,7 @@
                 Position.str_of pos)
             | SOME context => Context.proof_of context);
       
-          val lex = get_lexicon ();
+          val lex = #1 (OuterKeyword.get_lexicons ());
           fun no_decl _ = ("", "");
       
           fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state)