--- 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;
--- 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)