From bf211c52fd8fa79c8733fdaf1a127564c33a9829 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Thu, 24 Jan 2008 23:56:45 +0000
Subject: Remove use of proof-ass

---
 coq/x-symbol-coq.el   | 5 +++--
 isar/x-symbol-isar.el | 4 ++--
 phox/phox.el          | 2 +-
 phox/x-symbol-phox.el | 2 +-
 4 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el
index 44bb4925..c9abbcc8 100644
--- a/coq/x-symbol-coq.el
+++ b/coq/x-symbol-coq.el
@@ -13,6 +13,7 @@
 ;;
 
 (eval-when-compile
+  (require 'proof-utils)		; to properly compile 'proof-ass'
   (require 'cl))			; to properly compile 'block'
 
 (defvar x-symbol-coq-required-fonts nil)
@@ -162,7 +163,7 @@ or subscript tag."
 			 )))))
    
 (defun coq-match-subscript (limit)
-  (if (proof-ass x-symbol-enable)
+  (if coq-x-symbol-enable
       (setq x-symbol-coq-subscript-type
             (funcall x-symbol-coq-subscript-matcher limit))))
 
@@ -475,7 +476,7 @@ and `x-symbol-coq-xsymbol-table'."
     x-symbol-coq-xsymbol-table)))
 
 (defcustom x-symbol-coq-auto-style
-  '((proof-ass x-symbol-enable)	 ; MODE-ON: whether to turn on interactively
+  '(coq-x-symbol-enable	          ; MODE-ON: whether to turn on interactively
     nil   ;; x-symbol-coding
     'null ;; x-symbol-8bits	   [NEVER want it; null disables search]
     nil   ;; x-symbol-unique
diff --git a/isar/x-symbol-isar.el b/isar/x-symbol-isar.el
index d7ec9196..6a8a8fbf 100644
--- a/isar/x-symbol-isar.el
+++ b/isar/x-symbol-isar.el
@@ -156,7 +156,7 @@ or subscript tag."
 	      (return script-type))))))))
    
 (defun isabelle-match-subscript (limit)
-  (if (proof-ass x-symbol-enable)
+  (if isar-x-symbol-enable
       (setq x-symbol-isar-subscript-type
             (funcall x-symbol-isar-subscript-matcher limit))))
 
@@ -478,7 +478,7 @@ See `x-symbol-language-access-alist' for details."
 ;;
 ;; this is MODE-ON CODING 8BITS UNIQUE SUBSCRIPTS IMAGE
 (defcustom x-symbol-isar-auto-style
-  '((proof-ass x-symbol-enable)	 ; MODE-ON: whether to turn on interactively
+  '(isar-x-symbol-enable	   ; MODE-ON: whether to turn on interactively
     nil   ;; x-symbol-coding
     'null ;; x-symbol-8bits	   [NEVER want it; null disables search]
     nil   ;; x-symbol-unique
diff --git a/phox/phox.el b/phox/phox.el
index 6edae61d..a26f0105 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -252,7 +252,7 @@
  ;; internal completion table if completion is already active
 '(progn
    (defpgdefault completion-table
-     (append (proof-ass completion-table)
+     (append phox-completion-table
 	     (mapcar (lambda (xsym) (nth 2 xsym))
 		     x-symbol-phox-table)))
    (setq proof-xsym-font-lock-keywords
diff --git a/phox/x-symbol-phox.el b/phox/x-symbol-phox.el
index 7acd776f..8590dd23 100644
--- a/phox/x-symbol-phox.el
+++ b/phox/x-symbol-phox.el
@@ -183,7 +183,7 @@ See `x-symbol-language-access-alist' for details."
 ;;
 ;; this is MODE-ON CODING 8BITS UNIQUE SUBSCRIPTS IMAGE
 (defcustom x-symbol-phox-auto-style
-  '((proof-ass x-symbol-enable)	 ; MODE-ON: whether to turn on interactively
+  '(phox-x-symbol-enable	 ; MODE-ON: whether to turn on interactively
     nil   ;; x-symbol-coding
     'null ;; x-symbol-8bits	   [NEVER want it; null disables search]
     nil   ;; x-symbol-unique
-- 
cgit v1.2.3