1.1 --- a/src/HOL/SMT/Tools/z3_proof_tools.ML	Wed May 12 23:53:59 2010 +0200
     1.2 +++ b/src/HOL/SMT/Tools/z3_proof_tools.ML	Wed May 12 23:54:00 2010 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    val unfold_eqs: Proof.context -> thm list -> conv
     1.5    val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
     1.6    val by_tac: (int -> tactic) -> cterm -> thm
     1.7 -  val make_hyp_def: thm -> cterm list * thm
     1.8 +  val make_hyp_def: thm -> Proof.context -> thm * Proof.context
     1.9    val by_abstraction: Proof.context -> thm list -> (Proof.context -> cterm ->
    1.10      thm) -> cterm -> thm
    1.11  
    1.12 @@ -103,7 +103,7 @@
    1.13  fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
    1.14  
    1.15  (* |- c x == t x ==> P (c x)  ~~>  c == t |- P (c x) *) 
    1.16 -fun make_hyp_def thm =
    1.17 +fun make_hyp_def thm ctxt =
    1.18    let
    1.19      val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
    1.20      val (cf, cvs) = Drule.strip_comb lhs
    1.21 @@ -111,7 +111,10 @@
    1.22      fun apply cv th =
    1.23        Thm.combination th (Thm.reflexive cv)
    1.24        |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
    1.25 -  in ([eq], Thm.implies_elim thm (fold apply cvs (Thm.assume eq))) end
    1.26 +  in
    1.27 +    yield_singleton Assumption.add_assumes eq ctxt
    1.28 +    |>> Thm.implies_elim thm o fold apply cvs
    1.29 +  end
    1.30  
    1.31  
    1.32  
    1.33 @@ -336,7 +339,7 @@
    1.34  in
    1.35  
    1.36  fun make_simpset ctxt rules = Simplifier.context ctxt (HOL_ss
    1.37 -  addsimps @{thms ring_distribs} addsimps @{thms field_simps}
    1.38 +  addsimps @{thms field_simps}
    1.39    addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
    1.40    addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
    1.41    addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}