# HG changeset patch
# User blanchet
# Date 1399230141 -7200
# Node ID e7a55d295b8e45cf3b36e22271d7d906aad64e3f
# Parent  ddd3af5a683d8af669a5e5da14887cffb92fc545
simplify unused universally quantified variables in Z3 proofs

diff -r ddd3af5a683d -r e7a55d295b8e src/HOL/Tools/SMT2/z3_new_isar.ML
--- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Sun May 04 19:27:28 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Sun May 04 21:02:21 2014 +0200
@@ -63,7 +63,11 @@
           end
       end
 
-fun simplify_bool (@{const Not} $ t) = s_not (simplify_bool t)
+fun simplify_bool ((all as Const (@{const_name All}, _)) $ Abs (s, T, t)) =
+    let val t' = simplify_bool t in
+      if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t'
+    end
+  | simplify_bool (@{const Not} $ t) = s_not (simplify_bool t)
   | simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u)
   | simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u)
   | simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u)