changeset 66136 | dd006934a719 |
parent 66134 | a1fb6beb2731 |
child 66551 | 4df6b0ae900d |
--- a/src/HOL/Tools/SMT/smt_translate.ML Tue Jun 20 14:41:29 2017 +0200 +++ b/src/HOL/Tools/SMT/smt_translate.ML Tue Jun 20 14:41:35 2017 +0200 @@ -212,7 +212,7 @@ | expand t = (case Term.strip_comb t of (Const (@{const_name Let}, _), t1 :: t2 :: ts) => - betapplys (Term.betapply (expand t2, expand t1), map expand ts) + Term.betapplys (Term.betapply (expand t2, expand t1), map expand ts) | (u as Const (c as (_, T)), ts) => (case SMT_Builtin.dest_builtin ctxt c ts of SOME (_, k, us, mk) =>