--- a/src/HOL/Num.thy Fri Apr 10 11:29:12 2015 +0200
+++ b/src/HOL/Num.thy Fri Apr 10 11:31:10 2015 +0200
@@ -1195,10 +1195,10 @@
declaration {*
let
- 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;
in
K (
Lin_Arith.add_simps (@{thms arith_simps} @ @{thms more_arith_simps}