src/HOL/Tools/lin_arith.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59656 ddc5411c1cb9
     1.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -62,8 +62,8 @@
     1.4  
     1.5  fun mk_nat_thm thy t =
     1.6    let
     1.7 -    val cn = Thm.cterm_of thy (Var (("n", 0), HOLogic.natT))
     1.8 -    and ct = Thm.cterm_of thy t
     1.9 +    val cn = Thm.global_cterm_of thy (Var (("n", 0), HOLogic.natT))
    1.10 +    and ct = Thm.global_cterm_of thy t
    1.11    in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end;
    1.12  
    1.13  end;