src/HOL/Tools/SMT/smt_translate.ML
changeset 66136 dd006934a719
parent 66134 a1fb6beb2731
child 66551 4df6b0ae900d
     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) =>