src/Pure/Isar/attrib.ML
changeset 68816 5a53724fe247
parent 68558 7aae213d9e69
child 68823 5e7b1ae10eb8
--- a/src/Pure/Isar/attrib.ML	Mon Aug 27 14:31:52 2018 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Aug 27 14:42:24 2018 +0200
@@ -587,6 +587,9 @@
   register_config Name_Space.names_short_raw #>
   register_config Name_Space.names_unique_raw #>
   register_config ML_Print_Depth.print_depth_raw #>
+  register_config ML_Env.ML_environment_raw #>
+  register_config ML_Env.ML_read_global_raw #>
+  register_config ML_Env.ML_write_global_raw #>
   register_config ML_Options.source_trace_raw #>
   register_config ML_Options.exception_trace_raw #>
   register_config ML_Options.exception_debugger_raw #>