# HG changeset patch
# User wenzelm
# Date 1117533213 -7200
# Node ID 8eead5356ccb43ab5b57231272da1cb87f175513
# Parent  1e2bed9c06f794f76adacf8566b049602f31da33
added short_names, unique_names options;

diff -r 1e2bed9c06f7 -r 8eead5356ccb src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Tue May 31 11:53:32 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML	Tue May 31 11:53:33 2005 +0200
@@ -299,6 +299,8 @@
   ("show_structs", Library.setmp show_structs o boolean),
   ("show_question_marks", Library.setmp show_question_marks o boolean),
   ("long_names", Library.setmp NameSpace.long_names o boolean),
+  ("short_names", Library.setmp NameSpace.short_names o boolean),
+  ("unique_names", Library.setmp NameSpace.unique_names o boolean),
   ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
   ("locale", Library.setmp locale),
   ("display", Library.setmp display o boolean),