--- a/src/HOL/Tools/meson.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/meson.ML Sun Feb 28 23:51:31 2010 +0100
@@ -517,10 +517,10 @@
nnf_ss also includes the one-point simprocs,
which are needed to avoid the various one-point theorems from generating junk clauses.*)
val nnf_simps =
- [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
- if_False, if_cancel, if_eq_cancel, cases_simp];
+ [@{thm simp_implies_def}, @{thm Ex1_def}, @{thm Ball_def},@{thm Bex_def}, @{thm if_True},
+ @{thm if_False}, @{thm if_cancel}, @{thm if_eq_cancel}, @{thm cases_simp}];
val nnf_extra_simps =
- thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
+ @{thms split_ifs} @ @{thms ex_simps} @ @{thms all_simps} @ @{thms simp_thms};
val nnf_ss =
HOL_basic_ss addsimps nnf_extra_simps
@@ -685,7 +685,7 @@
(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
double-negations.*)
-val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
+val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection];
(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
fun select_literal i cl = negate_head (make_last i cl);