--- 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
--- 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)