--- a/src/HOL/Tools/meson.ML Thu Jul 29 16:11:02 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Jul 29 16:41:32 2010 +0200
@@ -14,6 +14,7 @@
val too_many_clauses: Proof.context option -> term -> bool
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
val finish_cnf: thm list -> thm list
+ val presimplify: thm -> thm
val make_nnf: Proof.context -> thm -> thm
val skolemize: Proof.context -> thm -> thm
val is_fol_term: theory -> term -> bool
@@ -529,9 +530,12 @@
HOL_basic_ss addsimps nnf_extra_simps
addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
+val presimplify =
+ rewrite_rule (map safe_mk_meta_eq nnf_simps)
+ #> simplify nnf_ss
+
fun make_nnf ctxt th = case prems_of th of
- [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
- |> simplify nnf_ss
+ [] => th |> presimplify
|> make_nnf1 ctxt
| _ => raise THM ("make_nnf: premises in argument", 0, [th]);