--- 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' (!?) *)