# HG changeset patch
# User aspinall
# Date 1102944662 -3600
# Node ID 9e58e666074df9e0bf97fbec9a66e683b48c2ede
# Parent  97204f3b4705a2cf41eea692909ea3ff6117582c
Fix pgmlsymbolson/off.

diff -r 97204f3b4705 -r 9e58e666074d src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Sun Dec 12 16:25:47 2004 +0100
+++ b/src/Pure/proof_general.ML	Mon Dec 13 14:31:02 2004 +0100
@@ -90,8 +90,8 @@
     (* NB: an alternative here would be to output the default print mode alternative
        in the element content, but unfortunately print modes are not that fine grained. *)
     Symbol.Char s => XML.text s
-  | Symbol.Sym s => XML.element "sym" [("name", s)] [XML.text s]
-  | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []  (* FIXME: no such PGML! *)
+  | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
+  | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s]   (* FIXME: no such PGML! *)
   | Symbol.Raw s => s);
 
 fun pgml_output str =
@@ -1154,10 +1154,8 @@
      | "proverexit" 	=> isarcmd "quit"
      | "startquiet" 	=> isarcmd "disable_pr"
      | "stopquiet"  	=> isarcmd "enable_pr"
-     | "pgmlsymbolson"   => (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
-     | "pgmlsymbolsoff"  => (print_mode := (Library.gen_rems 
-						(op =) 
-						(! print_mode, ["xsymbols", "symbols"])))
+     | "pgmlsymbolson"   => (print_mode := !print_mode @ ["xsymbols"])
+     | "pgmlsymbolsoff"  => (print_mode := (!print_mode \ "xsymbols"))
      (* properproofcmd: proper commands which belong in script *)
      (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
      | "opengoal"       => isarscript data