src/Pure/ML/ml_env.ML

--- a/src/Pure/ML/ml_env.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/ML/ml_env.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -9,11 +9,8 @@
 sig
   val Isabelle: string
   val SML: string
-  val ML_environment_raw: Config.raw
   val ML_environment: string Config.T
-  val ML_read_global_raw: Config.raw
   val ML_read_global: bool Config.T
-  val ML_write_global_raw: Config.raw
   val ML_write_global: bool Config.T
   val inherit: Context.generic list -> Context.generic -> Context.generic
   type operations =
@@ -48,17 +45,13 @@
 val Isabelle = "Isabelle";
 val SML = "SML";
 
-val ML_environment_raw = Config.declare ("ML_environment", \<^here>) (fn _ => Config.String Isabelle);
-val ML_environment = Config.string ML_environment_raw;
+val ML_environment = Config.declare_string ("ML_environment", \<^here>) (K Isabelle);
 
 
 (* global read/write *)
 
-val ML_read_global_raw = Config.declare ("ML_read_global", \<^here>) (fn _ => Config.Bool true);
-val ML_write_global_raw = Config.declare ("ML_write_global", \<^here>) (fn _ => Config.Bool true);
-
-val ML_read_global = Config.bool ML_read_global_raw;
-val ML_write_global = Config.bool ML_write_global_raw;
+val ML_read_global = Config.declare_bool ("ML_read_global", \<^here>) (K true);
+val ML_write_global = Config.declare_bool ("ML_write_global", \<^here>) (K true);
 
 fun read_global context = Config.get_generic context ML_read_global;
 fun write_global context = Config.get_generic context ML_write_global;