       ["Evaluate Region" sw:evaluate-region (mark)]
       ["ctext Spec" sw:set-swe-spec t]
       ["cd to this directory" cd-current-directory t] 
+      ["Generate Isabelle Obligation Theory" sw:convert-spec-to-isa-thy t]
       "-----"
       ["Find Definition" sw:meta-point t]
       ["Find Importing Spec" sw:find-importing-specs t]

With an argument, it doesn't convert imports."
  (interactive "P")
  (save-buffer)
  (let* ((filename (sw:containing-specware-unit-id nil))
	 (thy-file (sw:eval-in-lisp
		    (format
		     "(let ((TypeObligations::generateTerminationConditions? nil)

    (sw:add-specware-to-isabelle-path)
    (find-file-other-window thy-file)))

(defun sw:regenerate-isa-theories-for-uid ()
  "Regenerate Isabelle/HOL theories for unit."
  (interactive)
  (save-buffer)
  (let* ((filename (sw:containing-specware-unit-id t))
	 (thy-file (sw:eval-in-lisp
		    (format
		     "(let ((TypeObligations::generateTerminationConditions? nil)
                            (TypeObligations::generateExhaustivityConditions? nil)
                            (Prover::treatNatSpecially? nil))
                        (IsaTermPrinter::deleteThyFilesForUID %S)
                        (IsaTermPrinter::printUIDtoThyFile-2 %S t))"
		     filename filename)))
	 (revert-without-query (cons ".*.thy" revert-without-query))
	 (display-warning-suppressed-classes (cons 'warning
						   display-warning-suppressed-classes))
	 (buf (find-file-noselect thy-file t)))
    (kill-buffer buf)		; Because of x-symbol problems if it already exists
    (sw:add-specware-to-isabelle-path)
    (find-file-other-window thy-file)))

(defun sw:add-specware-to-isabelle-path ()
  (when (fboundp 'proof-shell-invisible-command)
    (proof-shell-ready-prover)
