src/Provers/Arith/cancel_numerals.ML

   val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*)
 end;
 
 signature CANCEL_NUMERALS =
 sig
-  val proc: Proof.context -> term -> thm option
+  val proc: Proof.context -> cterm -> thm option
 end;
 
 functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
 struct
 

               let val (_,u) = Data.dest_coeff t
               in if Termtab.defined tab2 u then u else seek terms end
   in  seek terms1 end;
 
 (*the simplification procedure*)
-fun proc ctxt t =
+fun proc ctxt ct =
   let
     val prems = Simplifier.prems_of ctxt
+    val t = Thm.term_of ct
     val ([t'], ctxt') = Variable.import_terms true [t] ctxt
     val export = singleton (Variable.export ctxt' ctxt)
     (* FIXME ctxt vs. ctxt' (!?) *)
 
     val (t1,t2) = Data.dest_bal t'