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