src/Pure/ML/ml_context.ML

--- a/src/Pure/ML/ml_context.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -17,8 +17,6 @@
   val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
     theory -> theory
   val print_antiquotations: Proof.context -> unit
-  val source_trace_raw: Config.raw
-  val source_trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
@@ -137,9 +135,6 @@
         in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
   in ((ml_env @ end_env, ml_body), opt_ctxt') end;
 
-val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
-val source_trace = Config.bool source_trace_raw;
-
 fun eval flags pos ants =
   let
     val non_verbose = {SML = #SML flags, verbose = false};
@@ -149,7 +144,7 @@
     val _ =
       (case Option.map Context.proof_of env_ctxt of
         SOME ctxt =>
-          if Config.get ctxt source_trace andalso Context_Position.is_visible ctxt
+          if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt
           then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
           else ()
       | NONE => ());