From 2b4eef78f93be6447e63ecb2270f3d798f877225 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel <makarius@sketis.net>
Date: Wed, 31 Aug 2011 18:18:21 +0000
Subject: clarified isar-improper-regexp -- "prems" is already reported as
 legacy by the prover (after Isabelle2011);

---
 isar/isar-syntax.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'isar')

diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 45ad87f9..340f2e96 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -216,7 +216,7 @@ Group number 1 matches the identifier possibly with quotes; group number 2
 matches contents of quotes for quoted identifiers.")
 
 (defconst isar-improper-regexp
-  "\\(\\<[A-Za-z][A-Za-z0-9'_]*_tac\\>\\|\\<goal[0-9]+\\>\\|\\<prems\\>\\)"
+  "\\(\\<[A-Za-z][A-Za-z0-9'_]*_tac\\>\\|\\<goal[0-9]+\\>\\)"
   "Regexp matching low-level features")
 
 (defconst isar-save-command-regexp
-- 
cgit v1.2.3