# HG changeset patch
# User wenzelm
# Date 1185980143 -7200
# Node ID 39b407fd6e8239896b50145d29474a4dd5a25547
# Parent  1b0bc10019a567078e777fd9ffeef46d99d5fd54
renamed 'print_options' to 'print_configs';

diff -r 1b0bc10019a5 -r 39b407fd6e82 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Aug 01 16:55:42 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Aug 01 16:55:43 2007 +0200
@@ -78,7 +78,7 @@
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_abbrevs: Toplevel.transition -> Toplevel.transition
   val print_facts: Toplevel.transition -> Toplevel.transition
-  val print_options: Toplevel.transition -> Toplevel.transition
+  val print_configs: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
   val print_locale: bool * (Locale.expr * Element.context list)
@@ -437,8 +437,8 @@
   ProofContext.setmp_verbose
     ProofContext.print_lthms (Toplevel.context_of state));
 
-val print_options = Toplevel.unknown_context o Toplevel.keep (fn state =>
-  ConfigOption.print_options (Toplevel.context_of state));
+val print_configs = Toplevel.unknown_context o Toplevel.keep (fn state =>
+  Attrib.print_configs (Toplevel.context_of state));
 
 val print_theorems_proof = Toplevel.keep (fn state =>
   ProofContext.setmp_verbose
diff -r 1b0bc10019a5 -r 39b407fd6e82 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 01 16:55:42 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 01 16:55:43 2007 +0200
@@ -731,9 +731,9 @@
   OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
 
-val print_optionsP =
-  OuterSyntax.improper_command "print_options" "print configuration options" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_options));
+val print_configsP =
+  OuterSyntax.improper_command "print_configs" "print configuration options" K.diag
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
 
 val print_contextP =
   OuterSyntax.improper_command "print_context" "print theory context name" K.diag
@@ -1013,7 +1013,7 @@
   interpretP,
   (*diagnostic commands*)
   pretty_setmarginP, helpP, print_classesP, print_commandsP,
-  print_optionsP, print_contextP, print_theoryP, print_syntaxP,
+  print_configsP, print_contextP, print_theoryP, print_syntaxP,
   print_abbrevsP, print_factsP, print_theoremsP, print_localesP,
   print_localeP, print_registrationsP, print_attributesP,
   print_simpsetP, print_rulesP, print_induct_rulesP,