diff -r 045187fc7840 -r aa7ca36d67fd src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Tools/numeral.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -40,7 +40,7 @@
 val oneT = Thm.ctyp_of_term one;
 
 val number_of = @{cpat "number_of"};
-val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
+val numberT = Thm.ctyp_of (the_context ()) (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
 
 fun instT T V = Thm.instantiate_cterm ([(V, T)], []);