--- a/src/HOL/SMT/Tools/smt_normalize.ML Thu Feb 11 09:14:34 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Thu Feb 11 17:48:55 2010 +0100
@@ -125,8 +125,15 @@
Conv.rewr_conv @{thm atomize_all}
| _ => Conv.all_conv) ct
+fun unfold_quants_conv ctxt =
+ let
+ val rules = [@{thm Ex1_def}, @{thm Ball_def}, @{thm Bex_def}]
+ val unfold_conv = Conv.try_conv (More_Conv.rewrs_conv rules)
+ in More_Conv.top_conv (K unfold_conv) ctxt end
+
fun normalize_rule ctxt =
Conv.fconv_rule (
+ unfold_quants_conv ctxt then_conv
Thm.beta_conversion true then_conv
Thm.eta_conversion then_conv
norm_binder_conv ctxt) #>