tuned signature;

--- 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}

--- 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]

--- a/src/HOL/Tools/lin_arith.ML	Fri Apr 10 11:29:12 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri Apr 10 11:31:10 2015 +0200
@@ -16,7 +16,7 @@
   val add_simprocs: simproc list -> Context.generic -> Context.generic
   val add_inj_const: string * typ -> Context.generic -> Context.generic
   val add_discrete_type: string -> Context.generic -> Context.generic
-  val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
+  val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic
   val setup: Context.generic -> Context.generic
   val global_setup: theory -> theory
   val split_limit: int Config.T

--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Apr 10 11:29:12 2015 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Apr 10 11:31:10 2015 +0200
@@ -91,16 +91,16 @@
   val map_data:
     ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
       lessD: thm list, neqE: thm list, simpset: simpset,
-      number_of: (theory -> typ -> int -> cterm) option} ->
+      number_of: (Proof.context -> typ -> int -> cterm) option} ->
      {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
       lessD: thm list, neqE: thm list, simpset: simpset,
-      number_of: (theory -> typ -> int -> cterm) option}) ->
+      number_of: (Proof.context -> typ -> int -> cterm) option}) ->
       Context.generic -> Context.generic
   val add_inj_thms: thm list -> Context.generic -> Context.generic
   val add_lessD: thm -> Context.generic -> Context.generic
   val add_simps: thm list -> Context.generic -> Context.generic
   val add_simprocs: simproc list -> Context.generic -> Context.generic
-  val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
+  val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic
 end;
 
 functor Fast_Lin_Arith
@@ -119,7 +119,7 @@
     lessD: thm list,
     neqE: thm list,
     simpset: simpset,
-    number_of: (theory -> typ -> int -> cterm) option};
+    number_of: (Proof.context -> typ -> int -> cterm) option};
 
   val empty : T =
    {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
@@ -169,7 +169,7 @@
 
 fun number_of ctxt =
   (case Data.get (Context.Proof ctxt) of
-    {number_of = SOME f, ...} => f (Proof_Context.theory_of ctxt)
+    {number_of = SOME f, ...} => f ctxt
   | _ => fn _ => fn _ => raise CTERM ("number_of", []));