From 39e2cc196ed9ef9bf7d9f444b47800368872bd0f Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Wed, 18 Aug 1999 17:05:22 +0000
Subject: deactivated isar-font-lock-terms (currently useless);

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

diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index b41a65c8..29342b28 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -149,7 +149,8 @@
 
 (defvar isar-font-lock-keywords-1
   (append
-   isar-font-lock-terms
+;FIXME n.a.
+;   isar-font-lock-terms
    (list
     (cons (proof-ids-to-regexp isar-keywords-minor) 'font-lock-type-face)
     (cons (proof-ids-to-regexp isar-keywords-control) 'proof-error-face)
-- 
cgit v1.2.3