--- a/src/HOL/Tools/int_arith.ML Fri Apr 10 11:29:12 2015 +0200
+++ b/src/HOL/Tools/int_arith.ML Fri Apr 10 11:31:10 2015 +0200
@@ -79,10 +79,10 @@
make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
proc = sproc, identifier = []}
-fun number_of thy T n =
- if not (Sign.of_sort thy (T, @{sort numeral}))
+fun number_of ctxt T n =
+ if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral}))
then raise CTERM ("number_of", [])
- else Numeral.mk_cnumber (Thm.global_ctyp_of thy T) n;
+ else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
val setup =
Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]