# HG changeset patch
# User wenzelm
# Date 1379195938 -7200
# Node ID b19242603e926edab79c8db6412f3757ae16cba8
# Parent  f8147d885600722c37a25e00230c71d8c95a1938# Parent  3170b5eb9f5a22e3906fcaf925c10328d96c4634
merged

diff -r 3170b5eb9f5a -r b19242603e92 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sat Sep 14 23:52:36 2013 +0200
+++ b/etc/isar-keywords.el	Sat Sep 14 23:58:58 2013 +0200
@@ -102,6 +102,7 @@
     "from"
     "full_prf"
     "fun"
+    "fun_cases"
     "function"
     "guess"
     "have"
@@ -524,6 +525,7 @@
     "extract_type"
     "fixrec"
     "fun"
+    "fun_cases"
     "hide_class"
     "hide_const"
     "hide_fact"