src/HOL/Tools/SMT/smt_normalize.ML
changeset 51717 9e7d1c139569
parent 51575 907efc894051
child 54041 227908156cd2
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -479,10 +479,9 @@
     1.4    fun mk_number_eq ctxt i lhs =
     1.5      let
     1.6        val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
     1.7 -      val ss = HOL_ss
     1.8 -        addsimps [@{thm Int.int_numeral}]
     1.9 -      fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1       
    1.10 -    in Goal.norm_result (Goal.prove_internal [] eq tac) end
    1.11 +      val tac =
    1.12 +        Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm Int.int_numeral}]) 1
    1.13 +    in Goal.norm_result (Goal.prove_internal [] eq (K tac)) end
    1.14  
    1.15    fun ite_conv cv1 cv2 =
    1.16      Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
    1.17 @@ -539,13 +538,14 @@
    1.18          | NONE => false)
    1.19      | is_strange_number _ _ = false
    1.20  
    1.21 -  val pos_num_ss = HOL_ss
    1.22 -    addsimps [@{thm Num.numeral_One}]
    1.23 -    addsimps [@{thm Num.neg_numeral_def}]
    1.24 +  val pos_num_ss =
    1.25 +    simpset_of (put_simpset HOL_ss @{context}
    1.26 +      addsimps [@{thm Num.numeral_One}]
    1.27 +      addsimps [@{thm Num.neg_numeral_def}])
    1.28  
    1.29    fun norm_num_conv ctxt =
    1.30      SMT_Utils.if_conv (is_strange_number ctxt)
    1.31 -      (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv
    1.32 +      (Simplifier.rewrite (put_simpset pos_num_ss ctxt)) Conv.no_conv
    1.33  in
    1.34  
    1.35  fun normalize_numerals_conv ctxt =