# 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)