From 73375b71d50c9be41127d424b4868a5d0ccdba80 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Thu, 1 Sep 2005 14:18:10 +0000
Subject: tuned ML code for manipulating print_mode;

---
 isa/x-symbol-isa.el | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'isa')

diff --git a/isa/x-symbol-isa.el b/isa/x-symbol-isa.el
index d1ff4cb7..71dcb41e 100644
--- a/isa/x-symbol-isa.el
+++ b/isa/x-symbol-isa.el
@@ -12,9 +12,9 @@
 
 (setq proof-xsym-extra-modes '(thy-mode)
       proof-xsym-activate-command
-      "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode);"
+      "change print_mode (insert (op =) \"xsymbols\")"
       proof-xsym-deactivate-command
-      "print_mode := (! print_mode \\\\ [\"xsymbols\", \"symbols\"]);")
+      "change print_mode (remove (op =) \"xsymbols\")")
 
 
 
-- 
cgit v1.2.3