From 3af94770dad3d79ab3b2fe6b5138fdd1b98bd9c4 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 17 Jun 2004 21:32:45 +0000
Subject: Fix index number back for isar-undo-remove-regexp, change isar-remove
 instead.

---
 isar/isar-syntax.el | 2 +-
 isar/isar.el        | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 88ddd8f6..1fe541a6 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -394,7 +394,7 @@ matches contents of quotes for quoted identifiers.")
 (defconst isar-kill "kill;")
 
 (defun isar-remove (name)
-  (concat "init_toplevel; kill_thy \"" name "\";"))
+  (concat "init_toplevel; kill_thy " name ";"))
 
 (defun isar-undos (i)
   (if (> i 0) (concat "undos_proof " (int-to-string i) ";")
diff --git a/isar/isar.el b/isar/isar.el
index d3555896..5bbb6a6d 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -475,7 +475,7 @@ proof-shell-retract-files-regexp."
         (setq span nil))
        ;; theory: remove and exit
        ((proof-string-match isar-undo-remove-regexp str)
-        (setq ans (isar-remove (match-string 3 str)))
+        (setq ans (isar-remove (match-string 2 str)))
         (setq span nil))
        ;; context switch: kill
        ((proof-string-match isar-undo-kill-regexp str)
-- 
cgit v1.2.3