tuned
authorboehmes
Mon Sep 05 11:34:54 2011 +0200 (2011-09-05)
changeset 44718b656af4c9796
parent 44717 c9cf0780cd4f
child 44719 176adba0c35e
tuned
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/z3_proof_parser.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 05 11:28:10 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 05 11:34:54 2011 +0200
     1.3 @@ -475,8 +475,7 @@
     1.4      "op * = (%a b. nat (int a * int b))"
     1.5      "op div = (%a b. nat (int a div int b))"
     1.6      "op mod = (%a b. nat (int a mod int b))"
     1.7 -    by (auto intro!: ext simp add: nat_mult_distrib nat_div_distrib
     1.8 -      nat_mod_distrib)}
     1.9 +    by (fastsimp simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
    1.10  
    1.11    val ints = map mk_meta_eq @{lemma
    1.12      "int 0 = 0"
     2.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Sep 05 11:28:10 2011 +0200
     2.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Sep 05 11:34:54 2011 +0200
     2.3 @@ -148,13 +148,11 @@
     2.4  end
     2.5  
     2.6  local
     2.7 -  fun equal_var cv (_, cu) = (cv aconvc cu)
     2.8 -
     2.9    fun prep (ct, vars) (maxidx, all_vars) =
    2.10      let
    2.11        val maxidx' = maxidx + maxidx_of ct + 1
    2.12  
    2.13 -      fun part (v as (i, cv)) =
    2.14 +      fun part (i, cv) =
    2.15          (case AList.lookup (op =) all_vars i of
    2.16            SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
    2.17          | NONE =>