src/HOL/Tools/SMT/z3_proof_methods.ML
changeset 51717 9e7d1c139569
parent 46497 89ccf66aa73d
child 52732 b4da1f2ec73f
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4    in
     1.5      Z3_Proof_Tools.by_tac (
     1.6        CONVERSION (SMT_Utils.prop_conv conv)
     1.7 -      THEN' Simplifier.simp_tac HOL_ss)
     1.8 +      THEN' Simplifier.simp_tac (put_simpset HOL_ss ctxt))
     1.9    end
    1.10  
    1.11