From fb56b50542f57d10a7a2bfb50ad4181ba7b96793 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 10 Mar 2000 05:57:58 +0000
Subject: Docstrings

---
 isa/isa.el | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/isa/isa.el b/isa/isa.el
index 03c3b11d..00b2daeb 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -386,8 +386,7 @@ Resulting output from Isabelle will be parsed by Proof General."
   "Retract the theory file FILE. If interactive, use buffer-file-name.
 To prevent inconsistencies, scripting is deactivated before doing this. 
 So if scripting is active in an ML file which is not completely processed, 
-you will be asked to retract the file or process the remainder of it.  
-(If you process the rest of it it may subsequently be unlocked anyway). "
+you will be asked to retract the file or process the remainder of it."
   (interactive (list buffer-file-name))
   (proof-deactivate-scripting)
   (proof-shell-invisible-command
-- 
cgit v1.2.3