     (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)

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)

      ["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]
