Add identifier info command to toolbar

1 files changed, 6 insertions, 5 deletions

diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index d9cbdeb4..1807f691 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -216,16 +216,12 @@ to the default toolbar."
 (defalias 'proof-toolbar-context 'proof-ctxt)
 (defalias 'proof-toolbar-context-enable-p 'proof-shell-available-p)
 
-;; Info
-
-(defalias 'proof-toolbar-info 'proof-help)
-
 ;; Command
 
 (defalias 'proof-toolbar-command 'proof-minibuffer-cmd)
 (defalias 'proof-toolbar-command-enable-p 'proof-shell-available-p)
 
-;; Help
+;; Help  (I was an alias for this)
  
 (defun proof-toolbar-help ()
   (interactive)
@@ -236,6 +232,11 @@ to the default toolbar."
 (defalias 'proof-toolbar-find 'proof-find-theorems)
 (defalias 'proof-toolbar-find-enable-p 'proof-shell-available-p)
 
+;; Info
+ 
+(defalias 'proof-toolbar-info 'proof-query-identifier)
+(defalias 'proof-toolbar-info-enable-p 'proof-shell-available-p)
+
 ;; Visibility (not on toolbar)
 
 (defalias 'proof-toolbar-visibility 'pg-toggle-visibility)