src/HOL/Tools/numeral.ML
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59642 929984c529d3
     1.1 --- a/src/HOL/Tools/numeral.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/numeral.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -44,10 +44,10 @@
     1.4  val oneT = Thm.ctyp_of_cterm one;
     1.5  
     1.6  val numeral = @{cpat "numeral"};
     1.7 -val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral));
     1.8 +val numeralT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral));
     1.9  
    1.10  val uminus = @{cpat "uminus"};
    1.11 -val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm uminus));
    1.12 +val uminusT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm uminus));
    1.13  
    1.14  fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
    1.15