--- a/src/HOL/Tools/numeral.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/numeral.ML Fri Mar 06 15:58:56 2015 +0100
@@ -44,10 +44,10 @@
val oneT = Thm.ctyp_of_cterm one;
val numeral = @{cpat "numeral"};
-val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral));
+val numeralT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral));
val uminus = @{cpat "uminus"};
-val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm uminus));
+val uminusT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm uminus));
fun instT T V = Thm.instantiate_cterm ([(V, T)], []);