# HG changeset patch
# User ballarin
# Date 1229276716 -3600
# Node ID 712c5281d4a4b5196ddea8c0d07699d683ec716f
# Parent  1951b3dd1df8b5f4fc82a8b9a40d2042658c63e7
Fixed legacy locale keywords (went to ZF rather than default keywords file).

diff -r 1951b3dd1df8 -r 712c5281d4a4 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sun Dec 14 15:50:21 2008 +0100
+++ b/etc/isar-keywords-ZF.el	Sun Dec 14 18:45:16 2008 +0100
@@ -40,9 +40,6 @@
     "chapter"
     "class"
     "class_deps"
-    "class_interpret"
-    "class_interpretation"
-    "class_locale"
     "classes"
     "classrel"
     "codatatype"
@@ -352,7 +349,6 @@
     "axiomatization"
     "axioms"
     "class"
-    "class_locale"
     "classes"
     "classrel"
     "codatatype"
@@ -415,8 +411,7 @@
   '("inductive_cases"))
 
 (defconst isar-keywords-theory-goal
-  '("class_interpretation"
-    "corollary"
+  '("corollary"
     "instance"
     "interpretation"
     "lemma"
@@ -443,8 +438,7 @@
     "subsubsect"))
 
 (defconst isar-keywords-proof-goal
-  '("class_interpret"
-    "have"
+  '("have"
     "hence"
     "interpret"
     "invoke"))
diff -r 1951b3dd1df8 -r 712c5281d4a4 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sun Dec 14 15:50:21 2008 +0100
+++ b/etc/isar-keywords.el	Sun Dec 14 18:45:16 2008 +0100
@@ -45,6 +45,9 @@
     "chapter"
     "class"
     "class_deps"
+    "class_interpret"
+    "class_interpretation"
+    "class_locale"
     "classes"
     "classrel"
     "code_abort"
@@ -418,6 +421,7 @@
     "axiomatization"
     "axioms"
     "class"
+    "class_locale"
     "classes"
     "classrel"
     "code_abort"
@@ -501,6 +505,7 @@
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
+    "class_interpretation"
     "corollary"
     "cpodef"
     "function"
@@ -539,7 +544,8 @@
     "subsubsect"))
 
 (defconst isar-keywords-proof-goal
-  '("have"
+  '("class_interpret"
+    "have"
     "hence"
     "interpret"
     "invoke"))