src/HOL/Tools/SMT/smt_translate.ML
changeset 41172 a17c2d669c40
parent 41165 ceb81a08534e
child 41173 7c6178d45cc8
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 14:29:04 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 16:29:56 2010 +0100
     1.3 @@ -378,9 +378,7 @@
     1.4        | replace @{const True} = term_true
     1.5        | replace @{const False} = term_false
     1.6        | replace t = t
     1.7 -  in
     1.8 -    Term.map_aterms replace (HOLogic.dest_Trueprop (Thm.prop_of term_bool))
     1.9 -  end
    1.10 +  in Term.map_aterms replace (U.prop_of term_bool) end
    1.11  
    1.12  val fol_rules = [
    1.13    Let_def,
    1.14 @@ -609,8 +607,7 @@
    1.15  
    1.16      val (builtins, ts1) =
    1.17        ithms
    1.18 -      |> map (HOLogic.dest_Trueprop o Thm.prop_of o snd)
    1.19 -      |> map (Envir.eta_contract o Envir.beta_norm)
    1.20 +      |> map (Envir.beta_eta_contract o U.prop_of o snd)
    1.21        |> mark_builtins ctxt
    1.22  
    1.23      val ((dtyps, tr_context, ctxt1), ts2) =