# HG changeset patch
# User nipkow
# Date 1082027090 -7200
# Node ID 1acde8c391793b7d32a4c04145410b583ef30621
# Parent  03a827b7dbe8df55fdf79177525782ccfaecc6fb
"haspref" -> "oldhaspref" (David Aspinall)

diff -r 03a827b7dbe8 -r 1acde8c39179 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Thu Apr 15 09:33:12 2004 +0200
+++ b/src/Pure/proof_general.ML	Thu Apr 15 13:04:50 2004 +0200
@@ -323,7 +323,7 @@
 (* NB: the default returned here is actually the current value, so
    repeated uses of <askprefs> will not work correctly. *)
 fun show_options () = issue_pgip (map 
-  (fn (name, (descr, (ty, get, _))) => (XML.element "haspref"
+  (fn (name, (descr, (ty, get, _))) => (XML.element "oldhaspref"
     [("type", ty), ("descr", descr), ("default", get ())] [name])) (!options));
 
 fun set_option name value = (case assoc (!options, name) of