# HG changeset patch
# User paulson
# Date 962290252 -7200
# Node ID 300bd596d696e8d948c93a2e7c0c86037b1e7236
# Parent  b86ff604729f45aa7b857fb409bbeb9a37bba6c9
now freezes Vars in order to prevent errors in cases like these:

Goal "Suc (x + i + j) + ?q ?ii ?jj + k + x = xxx";
Goal "Suc (x + i + j) = x + f(?q i j) + k";
Goal "Suc (x + i + j) = x + ?q i j + k";
Goal "Suc (?q ?ii ?jj + i + j) + ?rq ?ii ?jj + k + ?q ?ii ?jj = xxx";

diff -r b86ff604729f -r 300bd596d696 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Thu Jun 29 12:19:27 2000 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Thu Jun 29 16:50:52 2000 +0200
@@ -69,7 +69,12 @@
 
 (*the simplification procedure*)
 fun proc sg _ t =
-  let val (t1,t2) = Data.dest_bal 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 (t1,t2) = Data.dest_bal t' 
       val terms1 = Data.dest_sum t1
       and terms2 = Data.dest_sum t2
       val u = find_common (terms1,terms2)
@@ -81,22 +86,23 @@
 	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
 		raise TERM("cancel_numerals", []) 
 	    else Data.prove_conv [Data.norm_tac] sg 
-			(t, 
+			(t', 
 			 Data.mk_bal (newshape(n1,terms1'), 
 				      newshape(n2,terms2')))
   in
-
       apsome Data.simplify_meta_eq
        (if n2<=n1 then 
 	    Data.prove_conv 
 	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
 		Data.numeral_simp_tac] sg
-	       (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2'))
+	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
+				 Data.mk_sum terms2'))
 	else
 	    Data.prove_conv 
 	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
 		Data.numeral_simp_tac] sg
-	       (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2'))))
+	       (t', Data.mk_bal (Data.mk_sum terms1', 
+				 newshape(n2-n1,terms2'))))
   end
   handle TERM _ => None
        | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
diff -r b86ff604729f -r 300bd596d696 src/Provers/Arith/combine_numerals.ML
--- 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)