author blanchet Fri Dec 04 14:15:16 2015 +0100 (2015-12-04) changeset 61782 7d754aca6a75 parent 61781 e1e6bb36b27a child 61783 7f36a8bfa822
removed needless complication for modern SMT solvers
```     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 03 15:33:01 2015 +0100
1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Dec 04 14:15:16 2015 +0100
1.3 @@ -319,14 +319,10 @@
1.4
1.5    val fol_rules = [
1.6      Let_def,
1.7 -    @{lemma "P = True == P" by (rule eq_reflection) simp},
1.8 -    @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
1.9 +    @{lemma "P = True == P" by (rule eq_reflection) simp}]
1.10
1.12
1.13 -  fun wrap_in_if pat t =
1.14 -    if pat then raise BAD_PATTERN () else @{const If (bool)} \$ t \$ @{const True} \$ @{const False}
1.15 -
1.16    fun is_builtin_conn_or_pred ctxt c ts =
1.17      is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse
1.18      is_some (SMT_Builtin.dest_builtin_pred ctxt c ts)
1.19 @@ -343,9 +339,10 @@
1.20        | (u as Const (@{const_name If}, _), [t1, t2, t3]) =>
1.21            if pat then raise BAD_PATTERN () else u \$ in_form t1 \$ in_term pat t2 \$ in_term pat t3
1.22        | (Const (c as (n, _)), ts) =>
1.23 -          if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t)
1.24 -          else if is_quant n then wrap_in_if pat (in_form t)
1.25 -          else Term.list_comb (Const c, map (in_term pat) ts)
1.26 +          if is_builtin_conn_or_pred ctxt c ts orelse is_quant n then
1.27 +            if pat then raise BAD_PATTERN () else in_form t
1.28 +          else
1.29 +            Term.list_comb (Const c, map (in_term pat) ts)
1.30        | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts)
1.31        | _ => t)
1.32
```