From 028397926a396c428fdf3ee1b608e5ffea2af6c7 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 20 Dec 2000 10:29:51 +0000
Subject: goalsave -> proof

---
 generic/pg-user.el | 2 +-
 isar/isar.el       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 9aba625f..0666b7b9 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -114,7 +114,7 @@ the proof script."
   (proof-maybe-save-point
    (let
       ((span (proof-last-goal-or-goalsave)))
-     (if (and span (not (eq (span-property span 'type) 'goalsave))
+     (if (and span (not (eq (span-property span 'type) 'proof))
 	      (< (span-end span) (proof-unprocessed-begin)))
 	 (progn
 	   (goto-char (span-start span))
diff --git a/isar/isar.el b/isar/isar.el
index fb7f33f0..d9e7e7a2 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -367,7 +367,7 @@ proof-shell-retract-files-regexp."
        ((or (eq (span-property span 'type) 'comment)
             (proof-string-match isar-undo-skip-regexp str)))
        ;; finished goal: undo
-       ((eq (span-property span 'type) 'goalsave)
+       ((eq (span-property span 'type) 'proof)
         (setq ans isar-undo))
        ;; open goal: skip and exit
        ((proof-string-match isar-goal-command-regexp str)
-- 
cgit v1.2.3