tuning
authorblanchet
Tue Jun 20 14:41:35 2017 +0200 (24 months ago)
changeset 66136dd006934a719
parent 66135 1451a32479ba
child 66144 8f1cbb77a70a
tuning
src/HOL/Tools/SMT/smt_translate.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 20 14:41:29 2017 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 20 14:41:35 2017 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4        | expand t =
     1.5            (case Term.strip_comb t of
     1.6              (Const (@{const_name Let}, _), t1 :: t2 :: ts) =>
     1.7 -            betapplys (Term.betapply (expand t2, expand t1), map expand ts)
     1.8 +            Term.betapplys (Term.betapply (expand t2, expand t1), map expand ts)
     1.9            | (u as Const (c as (_, T)), ts) =>
    1.10                (case SMT_Builtin.dest_builtin ctxt c ts of
    1.11                  SOME (_, k, us, mk) =>