 (defun sw:convert-spec-to-isa-thy (recursive?)
   (interactive "P")
   (save-buffer)
-  (let* ((filename (sw:containing-specware-unit-id))
+  (let* ((filename (sw:containing-specware-unit-id nil))
 	 (thy-file (sw:eval-in-lisp
 		    (format
 		     "(let ((TypeObligations::generateTerminationConditions? nil)
-                            (TypeObligations::generateExhaustivityConditions? nil))
+                            (TypeObligations::generateExhaustivityConditions? nil)
+                            (Prover::treatNatSpecially? nil))
                         (IsaTermPrinter::printUIDtoThyFile-2 %S %S))"
 		     filename
 		     (if recursive? "t" "nil"))))

	  (error "Can't find definition of %s in %s" qsym file)))
    (beginning-of-line)
    (recenter 4)
    (when (not (null (cdr *pending-specware-meta-point-results*)))
      (message "%S more definitions."
	       (length (cdr *pending-specware-meta-point-results*))))))

;; (defvar *specware-context-str* "cl-user::*specware-global-context*")
(defvar *specware-context-str* "(MonadicStateInternal::readGlobalVar \"GlobalContext\")")


(defun sw:dired-process-current-file ()
  (interactive)
  (let ((filename (sw::file-to-specware-unit-id (dired-get-filename) t)))
    (lisp-or-specware-command ":sw " "proc " filename)))

(defun sw:apropos-symbol ()
