diff -r 5f898411ce87 -r 5e94dfead1c2 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Wed Sep 09 14:47:41 2015 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Wed Sep 09 20:57:21 2015 +0200
@@ -38,7 +38,7 @@
 
 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
   sig
-  val proc: Proof.context -> term -> thm option
+  val proc: Proof.context -> cterm -> thm option
   end
 =
 struct
@@ -65,8 +65,9 @@
         | NONE => find_repeated (tab, t::past, terms);
 
 (*the simplification procedure*)
-fun proc ctxt t =
+fun proc ctxt ct =
   let
+    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' (!?) *)