# HG changeset patch
# User boehmes
# Date 1265906935 -3600
# Node ID 133be405a6f1bde83596de47f3ac21d1075b9232
# Parent  a0334d7fb0abbdb18c30924cba78c349a1fab75f
unfold quantifiers (Ball, Bex, Ex1)

diff -r a0334d7fb0ab -r 133be405a6f1 src/HOL/SMT/Tools/smt_normalize.ML
--- 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) #>