Fix to proof-defintset-fn so that correct current value is displayed.

1 files changed, 5 insertions, 3 deletions

diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 808247ce..03e09b82 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -837,9 +837,11 @@ Args as for the macro `proof-defintset', except will be evaluated."
 	      ,(concat "Set `" (symbol-name var) "' to ARG.
 This function simply uses customize-set-variable to set the variable.
 It was constructed with `proof-defintset-fn'.")
-	      (interactive ,(format "nValue for %s (int, currently %s):" 
-				     (symbol-name var)  
-				     (symbol-value var)))
+	      (interactive (list 
+			    (read-number 
+			     (format "Value for %s (int, currently %s): " 
+				     (symbol-name (quote ,var))
+				     (symbol-value (quote ,var))))))
 	      (customize-set-variable (quote ,var) arg))))
 
 (defmacro proof-defintset (var &optional othername)