--- a/src/Provers/Arith/cancel_numerals.ML Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Thu Jul 08 19:34:56 2004 +0200
@@ -47,7 +47,7 @@
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
sig
- val proc: Sign.sg -> thm list -> term -> thm option
+ val proc: Sign.sg -> simpset -> term -> thm option
end
=
struct
@@ -69,8 +69,10 @@
in seek terms1 end;
(*the simplification procedure*)
-fun proc sg hyps t =
- let (*first freeze any Vars in the term to prevent flex-flex problems*)
+fun proc sg ss t =
+ let
+ val hyps = prems_of_ss ss;
+ (*first freeze any Vars in the term to prevent flex-flex problems*)
val (t', xs) = Term.adhoc_freeze_vars t;
val (t1,t2) = Data.dest_bal t'
val terms1 = Data.dest_sum t1