--- 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
--- 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,