diff -r e79bc66572df -r 4dca48557921 src/HOL/Num.thy
--- 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}