# HG changeset patch
# User wenzelm
# Date 1132146341 -3600
# Node ID c6e3c6516a239e864cdf7a69547b1c308593b1b7
# Parent  8ae6a9e7ff0e7dd98610d76a94010c657ae263f0
pgmlsymbolson: append Symbol.xsymbolsN at end!

diff -r 8ae6a9e7ff0e -r c6e3c6516a23 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue Nov 15 14:08:32 2005 +0100
+++ b/src/Pure/proof_general.ML	Wed Nov 16 14:05:41 2005 +0100
@@ -1218,7 +1218,8 @@
      | "proverexit"     => isarcmd "quit"
      | "startquiet"     => isarcmd "disable_pr"
      | "stopquiet"      => isarcmd "enable_pr"
-     | "pgmlsymbolson"   => change print_mode (insert (op =) Symbol.xsymbolsN)
+     | "pgmlsymbolson"   => change print_mode (fn mode =>
+          remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN])
      | "pgmlsymbolsoff"  => change print_mode (remove (op =) Symbol.xsymbolsN)
      (* properproofcmd: proper commands which belong in script *)
      (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)