--- a/src/Provers/Arith/combine_numerals.ML Thu Jun 29 12:19:27 2000 +0200
+++ b/src/Provers/Arith/combine_numerals.ML Thu Jun 29 16:50:52 2000 +0200
@@ -64,13 +64,18 @@
(*the simplification procedure*)
fun proc sg _ t =
- let val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t)
+ let (*first freeze any Vars in the term to prevent flex-flex problems*)
+ val rand_s = gensym"_"
+ fun mk_inst (var as Var((a,i),T)) =
+ (var, Free((a ^ rand_s ^ string_of_int i), T))
+ val t' = subst_atomic (map mk_inst (term_vars t)) t
+ val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
val reshape = (*Move i*u to the front and put j*u into standard form
i + #m + j + k == #m + i + (j + k) *)
if m=0 orelse n=0 then (*trivial, so do nothing*)
raise TERM("combine_numerals", [])
else Data.prove_conv [Data.norm_tac] sg
- (t,
+ (t',
Data.mk_sum ([Data.mk_coeff(m,u),
Data.mk_coeff(n,u)] @ terms))
in
@@ -78,7 +83,7 @@
(Data.prove_conv
[Data.trans_tac reshape, rtac Data.left_distrib 1,
Data.numeral_simp_tac] sg
- (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
+ (t', Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
end
handle TERM _ => None
| TYPE _ => None; (*Typically (if thy doesn't include Numeral)