# HG changeset patch
# User wenzelm
# Date 1165683946 -3600
# Node ID 092b967da9b7f3cc27b9226ac38215518d38365f
# Parent  ec2014c93d7f1d3cc1bfa48b36bfa15acc8a5b56
added 'print_abbrevs';

diff -r ec2014c93d7f -r 092b967da9b7 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Dec 09 18:05:44 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 09 18:05:46 2006 +0100
@@ -690,9 +690,13 @@
     (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
 
 val print_syntaxP =
-  OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
+  OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
 
+val print_abbrevsP =
+  OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
+
 val print_theoremsP =
   OuterSyntax.improper_command "print_theorems"
       "print theorems of local theory or proof context" K.diag
@@ -938,13 +942,14 @@
   interpretationP, interpretP,
   (*diagnostic commands*)
   pretty_setmarginP, helpP, print_commandsP, print_contextP,
-  print_theoryP, print_syntaxP, print_factsP, print_theoremsP,
-  print_localesP, print_localeP, print_registrationsP,
-  print_attributesP, print_simpsetP, print_rulesP,
-  print_induct_rulesP, print_trans_rulesP, print_methodsP,
-  print_antiquotationsP, class_depsP, thm_depsP, find_theoremsP,
-  print_bindsP, print_casesP, print_stmtsP, print_thmsP, print_prfsP,
-  print_full_prfsP, print_propP, print_termP, print_typeP,
+  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, print_trans_rulesP,
+  print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
+  find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
+  print_thmsP, print_prfsP, print_full_prfsP, print_propP,
+  print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,