1.1 --- a/src/HOL/SMT/Tools/smt_translate.ML	Wed May 12 23:54:00 2010 +0200
     1.2 +++ b/src/HOL/SMT/Tools/smt_translate.ML	Wed May 12 23:54:01 2010 +0200
     1.3 @@ -144,36 +144,24 @@
     1.4  val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
     1.5  
     1.6  
     1.7 -val is_let = (fn Const (@{const_name Let}, _) $ _ $ Abs _ => true | _ => false)
     1.8 -
     1.9 -val is_true_eq = (fn
    1.10 -    @{term "op = :: bool => _"} $ _ $ @{term True} => true
    1.11 +val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
    1.12 +    Const (@{const_name Let}, _) => true
    1.13 +  | @{term "op = :: bool => _"} $ _ $ @{term True} => true
    1.14 +  | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
    1.15    | _ => false)
    1.16  
    1.17 -val true_eq_rewr = @{lemma "P = True == P" by simp}
    1.18 +val rewrite_rules = [
    1.19 +  Let_def,
    1.20 +  @{lemma "P = True == P" by (rule eq_reflection) simp},
    1.21 +  @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
    1.22  
    1.23 -val is_trivial_if = (fn
    1.24 -    Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
    1.25 -  | _ => false)
    1.26 -
    1.27 -val trivial_if_rewr = @{lemma "(if P then True else False) == P"
    1.28 -  by (atomize(full)) simp}
    1.29 -
    1.30 -fun rewrite _ ct =
    1.31 -  if is_trivial_if (Thm.term_of ct) then Conv.rewr_conv trivial_if_rewr ct
    1.32 -  else if is_true_eq (Thm.term_of ct) then Conv.rewr_conv true_eq_rewr ct
    1.33 -  else if is_let (Thm.term_of ct) then Conv.rewr_conv @{thm Let_def} ct
    1.34 -  else Conv.all_conv ct
    1.35 -
    1.36 -val needs_rewrite =
    1.37 -  Term.exists_subterm (is_trivial_if orf is_true_eq orf is_let)
    1.38 +fun rewrite ctxt = Simplifier.full_rewrite
    1.39 +  (Simplifier.context ctxt empty_ss addsimps rewrite_rules)
    1.40  
    1.41  fun normalize ctxt thm =
    1.42 -  if needs_rewrite (Thm.prop_of thm)
    1.43 -  then Conv.fconv_rule (More_Conv.top_conv rewrite ctxt) thm
    1.44 -  else thm
    1.45 +  if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm
    1.46  
    1.47 -val unfold_rules = [term_eq_rewr, Let_def, trivial_if_rewr, true_eq_rewr]
    1.48 +val unfold_rules = term_eq_rewr :: rewrite_rules
    1.49  
    1.50  
    1.51  val revert_types =