changeset 47207 | 9368aa814518 |
parent 47155 | ade3fc826af3 |
child 50601 | 74da81de127f |
--- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Mar 29 14:47:31 2012 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Mar 30 08:10:28 2012 +0200 @@ -467,7 +467,7 @@ let val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i) val ss = HOL_ss - addsimps [@{thm Nat_Numeral.int_numeral}] + addsimps [@{thm Int.int_numeral}] fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1 in Goal.norm_result (Goal.prove_internal [] eq tac) end