# HG changeset patch
# User wenzelm
# Date 1437141791 -7200
# Node ID 37d624a8b128c04c33fb4cf25478a559cae83226
# Parent  6349a28af772ad33643c1dd54a79a05f57d5ef3a
proper attribute;

diff -r 6349a28af772 -r 37d624a8b128 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jul 16 18:36:16 2015 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Jul 17 16:03:11 2015 +0200
@@ -527,6 +527,7 @@
   register_config Name_Space.names_unique_raw #>
   register_config ML_Options.source_trace_raw #>
   register_config ML_Options.exception_trace_raw #>
+  register_config ML_Options.debugger_raw #>
   register_config ML_Options.print_depth_raw #>
   register_config Proof_Context.show_abbrevs_raw #>
   register_config Goal_Display.goals_limit_raw #>