src/HOL/Tools/SMT/smt_normalize.ML
changeset 54883 dd04a8b654fc
parent 54489 03ff4d1e6784
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 31 11:19:14 2013 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 31 14:29:16 2013 +0100
     1.3 @@ -480,7 +480,7 @@
     1.4        val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
     1.5        val tac =
     1.6          Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm Int.int_numeral}]) 1
     1.7 -    in Goal.norm_result (Goal.prove_internal [] eq (K tac)) end
     1.8 +    in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
     1.9  
    1.10    fun ite_conv cv1 cv2 =
    1.11      Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2