diff -r cbc38731d42f -r 0fbed69ff081 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Tools/int_arith.ML	Wed Mar 04 19:53:18 2015 +0100
@@ -25,8 +25,8 @@
 val lhss0 = [@{cpat "0::?'a::ring"}];
 
 fun proc0 phi ctxt ct =
-  let val T = ctyp_of_term ct
-  in if typ_of T = @{typ int} then NONE else
+  let val T = Thm.ctyp_of_term ct
+  in if Thm.typ_of T = @{typ int} then NONE else
      SOME (instantiate' [SOME T] [] zeroth)
   end;
 
@@ -39,8 +39,8 @@
 val lhss1 = [@{cpat "1::?'a::ring_1"}];
 
 fun proc1 phi ctxt ct =
-  let val T = ctyp_of_term ct
-  in if typ_of T = @{typ int} then NONE else
+  let val T = Thm.ctyp_of_term ct
+  in if Thm.typ_of T = @{typ int} then NONE else
      SOME (instantiate' [SOME T] [] oneth)
   end;
 
@@ -67,7 +67,7 @@
      addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
 
 fun sproc phi ctxt ct =
-  if check (term_of ct) then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
+  if check (Thm.term_of ct) then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
   else NONE;
 
 val lhss' =