src/HOL/Tools/int_arith.ML
changeset 59586 ddf6deaadfe8
parent 59582 0fbed69ff081
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/int_arith.ML	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4  val lhss0 = [@{cpat "0::?'a::ring"}];
     1.5  
     1.6  fun proc0 phi ctxt ct =
     1.7 -  let val T = Thm.ctyp_of_term ct
     1.8 +  let val T = Thm.ctyp_of_cterm ct
     1.9    in if Thm.typ_of T = @{typ int} then NONE else
    1.10       SOME (instantiate' [SOME T] [] zeroth)
    1.11    end;
    1.12 @@ -39,7 +39,7 @@
    1.13  val lhss1 = [@{cpat "1::?'a::ring_1"}];
    1.14  
    1.15  fun proc1 phi ctxt ct =
    1.16 -  let val T = Thm.ctyp_of_term ct
    1.17 +  let val T = Thm.ctyp_of_cterm ct
    1.18    in if Thm.typ_of T = @{typ int} then NONE else
    1.19       SOME (instantiate' [SOME T] [] oneth)
    1.20    end;