# HG changeset patch
# User boehmes
# Date 1315215294 -7200
# Node ID b656af4c9796ad19db3ee6df2be3cc15d81bf09c
# Parent  c9cf0780cd4f63e1b633821550a8bb70b18c56b7
tuned

diff -r c9cf0780cd4f -r b656af4c9796 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 05 11:28:10 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 05 11:34:54 2011 +0200
@@ -475,8 +475,7 @@
     "op * = (%a b. nat (int a * int b))"
     "op div = (%a b. nat (int a div int b))"
     "op mod = (%a b. nat (int a mod int b))"
-    by (auto intro!: ext simp add: nat_mult_distrib nat_div_distrib
-      nat_mod_distrib)}
+    by (fastsimp simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
 
   val ints = map mk_meta_eq @{lemma
     "int 0 = 0"
diff -r c9cf0780cd4f -r b656af4c9796 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Sep 05 11:28:10 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Sep 05 11:34:54 2011 +0200
@@ -148,13 +148,11 @@
 end
 
 local
-  fun equal_var cv (_, cu) = (cv aconvc cu)
-
   fun prep (ct, vars) (maxidx, all_vars) =
     let
       val maxidx' = maxidx + maxidx_of ct + 1
 
-      fun part (v as (i, cv)) =
+      fun part (i, cv) =
         (case AList.lookup (op =) all_vars i of
           SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
         | NONE =>