Revert change in 10.26 to use defpacustom after all, this gives

the prover-specific menu entry automatically.  Fix compiler warning
with a defvar.

1 files changed, 9 insertions, 14 deletions

diff --git a/isar/isar.el b/isar/isar.el
index e2ddf4c2..c69d855f 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -24,6 +24,7 @@
   (require 'pg-vars)
   (defvar outline-heading-end-regexp nil)
   (defvar comment-quote-nested nil)
+  (defvar isar-use-find-theorems-form nil)
   (proof-ready-for-assistant 'isar))	; compile for isar
 
 (require 'isabelle-system)		; system code
@@ -240,25 +241,19 @@ See -k option for Isabelle interface script."
 ;;;
 
 
-(defun isar-use-find-theorems-form-set (sym val)
-  (set-default sym val)
-  (when (featurep 'isar) ; not during loading
-    (isar-set-proof-find-theorems-command)))
+(defun isar-configure-from-settings ()
+  (isar-set-proof-find-theorems-command))
 
-(defcustom isar-use-find-theorems-form nil
+(defpacustom use-find-theorems-form nil
   "Use a form-style input for the find theorems operation."
   :type 'boolean
-  :group 'isabelle
-  :set 'isar-use-find-theorems-form-set)
+  :eval (isar-set-proof-find-theorems-command))
 
 (defun isar-set-proof-find-theorems-command ()
-    (setq proof-find-theorems-command
-	  (if isar-use-find-theorems-form
-	      'isar-find-theorems-form
-	    'isar-find-theorems-minibuffer)))
-
-(defun isar-configure-from-settings ()
-  (isar-set-proof-find-theorems-command))
+  (setq proof-find-theorems-command
+	(if isar-use-find-theorems-form
+	    'isar-find-theorems-form
+	  'isar-find-theorems-minibuffer)))
 
 ;;;
 ;;; Theory loader operations