--- 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"
--- 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 =>