# HG changeset patch
# User wenzelm
# Date 1178638818 -7200
# Node ID 9ffb43b19ec68e7f27622d6d678fd3e2d329ec60
# Parent  c37e32bdbea274c31f2527a88ee5068fc8db3001
tuned;

diff -r c37e32bdbea2 -r 9ffb43b19ec6 NEWS
--- a/NEWS	Tue May 08 15:37:27 2007 +0200
+++ b/NEWS	Tue May 08 17:40:18 2007 +0200
@@ -19,8 +19,9 @@
 with Isar theories; migration is usually quite simple with the ML
 function use_legacy_bindings.  INCOMPATIBILITY.
 
-* Theory syntax: some popular names (e.g. "class", "fun", "help",
-"if") are now keywords.  INCOMPATIBILITY, use double quotes.
+* Theory syntax: some popular names (e.g. 'class', 'declaration',
+'fun', 'help', 'if') are now keywords.  INCOMPATIBILITY, use double
+quotes.
 
 * Legacy goal package: reduced interface to the bare minimum required
 to keep existing proof scripts running.  Most other user-level
diff -r c37e32bdbea2 -r 9ffb43b19ec6 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue May 08 15:37:27 2007 +0200
+++ b/src/HOL/Tools/meson.ML	Tue May 08 17:40:18 2007 +0200
@@ -240,7 +240,7 @@
 (*Any need to extend this list with 
   "HOL.type_class","Code_Generator.eq_class","ProtoPure.term"?*)
 val has_meta_conn = 
-    exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
+    exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
 
 fun apply_skolem_ths (th, rls) = 
   let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)