# HG changeset patch # User blanchet # Date 1449234916 -3600 # Node ID 7d754aca6a75df9bd49efb5c7601e0477f6ab8ee # Parent e1e6bb36b27a97f8bf508780957e83fed27e3931 removed needless complication for modern SMT solvers diff -r e1e6bb36b27a -r 7d754aca6a75 src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 03 15:33:01 2015 +0100 +++ b/src/HOL/Tools/SMT/smt_translate.ML Fri Dec 04 14:15:16 2015 +0100 @@ -319,14 +319,10 @@ val fol_rules = [ Let_def, - @{lemma "P = True == P" by (rule eq_reflection) simp}, - @{lemma "if P then True else False == P" by (rule eq_reflection) simp}] + @{lemma "P = True == P" by (rule eq_reflection) simp}] exception BAD_PATTERN of unit - fun wrap_in_if pat t = - if pat then raise BAD_PATTERN () else @{const If (bool)} $ t $ @{const True} $ @{const False} - fun is_builtin_conn_or_pred ctxt c ts = is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse is_some (SMT_Builtin.dest_builtin_pred ctxt c ts) @@ -343,9 +339,10 @@ | (u as Const (@{const_name If}, _), [t1, t2, t3]) => if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3 | (Const (c as (n, _)), ts) => - if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t) - else if is_quant n then wrap_in_if pat (in_form t) - else Term.list_comb (Const c, map (in_term pat) ts) + if is_builtin_conn_or_pred ctxt c ts orelse is_quant n then + if pat then raise BAD_PATTERN () else in_form t + else + Term.list_comb (Const c, map (in_term pat) ts) | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts) | _ => t)