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;

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

(limited to 'isar')

diff --git a/isar/x-symbol-isar.el b/isar/x-symbol-isar.el
index 42752ebe..684a2a21 100644
--- a/isar/x-symbol-isar.el
+++ b/isar/x-symbol-isar.el
@@ -13,10 +13,10 @@
 (setq
  proof-xsym-activate-command
  (isar-markup-ml 
-  "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode)")
+  "change print_mode (insert (op =) \"xsymbols\")")
  proof-xsym-deactivate-command
  (isar-markup-ml 
-  "print_mode := (Library.gen_rems (op =) (! print_mode, [\"xsymbols\", \"symbols\"]))"))
+  "change print_mode (remove (op =) \"xsymbols\")"))
 
 
 (provide 'x-symbol-isar)
-- 
cgit v1.2.3