Renamed some bound variables due to changes in simplifier.

--- a/src/ZF/CardinalArith.ML	Sun Nov 11 21:38:54 2001 +0100
+++ b/src/ZF/CardinalArith.ML	Mon Nov 12 10:37:36 2001 +0100
@@ -483,19 +483,19 @@
 by (etac ltE 2 THEN assume_tac 2);
 by (asm_full_simp_tac (simpset() addsimps [ordertype_unfold]) 1);
 by (safe_tac (claset() addSEs [ltE]));
-by (subgoals_tac ["Ord(xb)", "Ord(y)"] 1);
+by (subgoals_tac ["Ord(xa)", "Ord(ya)"] 1);
 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 2));
 by (rtac (InfCard_is_Limit RS ordermap_csquare_le RS lt_trans1) 1  THEN
     REPEAT (ares_tac [refl] 1 ORELSE etac ltI 1));
-by (res_inst_tac [("i","xb Un y"), ("j","nat")] Ord_linear2 1  THEN
+by (res_inst_tac [("i","xa Un ya"), ("j","nat")] Ord_linear2 1  THEN
     REPEAT (ares_tac [Ord_Un, Ord_nat] 1));
-(*the finite case: xb Un y < nat *)
+(*the finite case: xa Un ya < nat *)
 by (res_inst_tac [("j", "nat")] lt_trans2 1);
 by (asm_full_simp_tac (simpset() addsimps [InfCard_def]) 2);
 by (asm_full_simp_tac
     (simpset() addsimps [lt_def, nat_cmult_eq_mult, nat_succI, mult_type,
 			 nat_into_Card RS Card_cardinal_eq, Ord_nat]) 1);
-(*case nat le (xb Un y) *)
+(*case nat le (xa Un ya) *)
 by (asm_full_simp_tac
     (simpset() addsimps [le_imp_subset RS nat_succ_eqpoll RS cardinal_cong,
 			 le_succ_iff, InfCard_def, Card_cardinal, Un_least_lt, 

--- a/src/ZF/Induct/Multiset.ML	Sun Nov 11 21:38:54 2001 +0100
+++ b/src/ZF/Induct/Multiset.ML	Mon Nov 12 10:37:36 2001 +0100
@@ -555,10 +555,10 @@
 by (rotate_simp_tac "ALL a:A. ?u(a)" 1);
 by (subgoal_tac "setsum(%x. $# mcount(M, x), A)=$# succ(x)" 1);
 by (dtac setsum_succD 1 THEN Auto_tac);
-by (case_tac "1 <M`xa" 1);
+by (case_tac "1 <M`a" 1);
 by (dtac not_lt_imp_le 2);
 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nat_le_1_cases])));
-by (subgoal_tac "M=(M(xa:=M`xa #- 1))(xa:=(M(xa:=M`xa #- 1))`xa #+ 1)" 1);
+by (subgoal_tac "M=(M(a:=M`a #- 1))(a:=(M(a:=M`a #- 1))`a #+ 1)" 1);
 by (res_inst_tac [("A","A"),("B","%x. nat"),("D","%x. nat")] fun_extension 2);
 by (REPEAT(rtac update_type 3));
 by (ALLGOALS(Asm_simp_tac));
@@ -570,14 +570,14 @@
 by (res_inst_tac [("x", "A")] exI 1);
 by (force_tac (claset() addIs [update_type], simpset()) 1);
 by (asm_simp_tac (simpset() addsimps [mset_of_def, mcount_def]) 1);
-by (dres_inst_tac [("x", "M(xa := M ` xa #- 1)")] spec 1);
+by (dres_inst_tac [("x", "M(a := M ` a #- 1)")] spec 1);
 by (dtac mp 1 THEN dtac mp 2);
 by (ALLGOALS(Asm_full_simp_tac));
 by (res_inst_tac [("x", "A")] exI 1);
 by (auto_tac (claset() addIs [update_type], simpset()));
-by (subgoal_tac "Finite({x:cons(xa, A). x~=xa-->0<M`x})" 1);
+by (subgoal_tac "Finite({x:cons(a, A). x~=a-->0<M`x})" 1);
 by (blast_tac(claset() addIs [Collect_subset RS subset_Finite,Finite_cons])2);
-by (dres_inst_tac [("A", "{x:cons(xa, A). x~=xa-->0<M`x}")] setsum_decr 1);
+by (dres_inst_tac [("A", "{x:cons(a, A). x~=a-->0<M`x}")] setsum_decr 1);
 by (dres_inst_tac [("x", "M")] spec 1);
 by (subgoal_tac "multiset(M)" 1);
 by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
@@ -585,41 +585,41 @@
 by (Force_tac 2);
 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [mset_of_def])));
 by (dres_inst_tac [("psi", "ALL x:A. ?u(x)")] asm_rl 1);
-by (dres_inst_tac [("x", "xa")] bspec 1);
+by (dres_inst_tac [("x", "a")] bspec 1);
 by (Asm_simp_tac 1);
-by (subgoal_tac "cons(xa, A)= A" 1);
+by (subgoal_tac "cons(a, A)= A" 1);
 by (Blast_tac 2);
-by (rotate_simp_tac "cons(xa, A) = A" 1);
+by (rotate_simp_tac "cons(a, A) = A" 1);
 by (rotate_simp_tac "ALL x:A. ?u(x)" 1);
 by (rotate_simp_tac "ALL x:A. ?u(x)" 2);
-by (subgoal_tac "M=cons(<xa, M`xa>, restrict(M, A-{xa}))" 1);
+by (subgoal_tac "M=cons(<a, M`a>, restrict(M, A-{a}))" 1);
 by (rtac  fun_cons_restrict_eq 2);
-by (subgoal_tac "cons(xa, A-{xa}) = A" 2);
+by (subgoal_tac "cons(a, A-{a}) = A" 2);
 by (REPEAT(Force_tac 2));
-by (res_inst_tac [("a", "cons(<xa, 1>, restrict(M, A - {xa}))")] ssubst 1);
+by (res_inst_tac [("a", "cons(<a, 1>, restrict(M, A - {a}))")] ssubst 1);
 by (Asm_full_simp_tac 1);
-by (subgoal_tac "multiset(restrict(M, A - {xa}))" 1);
+by (subgoal_tac "multiset(restrict(M, A - {a}))" 1);
 by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
-by (res_inst_tac [("x", "A-{xa}")] exI 2);
+by (res_inst_tac [("x", "A-{a}")] exI 2);
 by Safe_tac;
-by (res_inst_tac [("A", "A-{xa}")] apply_type 3);
+by (res_inst_tac [("A", "A-{a}")] apply_type 3);
 by (asm_simp_tac (simpset() addsimps [restrict]) 5);
 by (REPEAT(blast_tac (claset() addIs [Finite_Diff, restrict_type]) 2));;
 by (resolve_tac prems 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [mset_of_def]) 1);
-by (dres_inst_tac [("x", "restrict(M, A-{xa})")] spec 1);
+by (dres_inst_tac [("x", "restrict(M, A-{a})")] spec 1);
 by (dtac mp 1);
-by (res_inst_tac [("x", "A-{xa}")] exI 1);
+by (res_inst_tac [("x", "A-{a}")] exI 1);
 by (auto_tac (claset() addIs [Finite_Diff, restrict_type], 
              simpset() addsimps [restrict]));
-by (forw_inst_tac [("A", "A"), ("M", "M"), ("a", "xa")] setsum_decr3 1);
+by (forw_inst_tac [("A", "A"), ("M", "M"), ("a", "a")] setsum_decr3 1);
 by (asm_simp_tac  (simpset() addsimps [multiset_def, multiset_fun_iff]) 1);
 by (Blast_tac 1);
 by (asm_simp_tac (simpset() addsimps [mset_of_def]) 1);
 by (dres_inst_tac [("b", "if ?u then ?v else ?w")] sym 1);
 by (ALLGOALS(rotate_simp_tac "ALL x:A. ?u(x)"));
-by (subgoal_tac "{x:A - {xa} . 0 < restrict(M, A - {x}) ` x} = A - {xa}" 1);
+by (subgoal_tac "{x:A - {a} . 0 < restrict(M, A - {x}) ` x} = A - {a}" 1);
 by (auto_tac (claset() addSIs [setsum_cong], 
               simpset() addsimps [zdiff_eq_iff, 
                zadd_commute, multiset_def, multiset_fun_iff,mset_of_def]));
@@ -824,7 +824,7 @@
 by (res_inst_tac [("x", "x")] bexI 3);
 by (res_inst_tac [("x", "xb")] bexI 3);
 by (Asm_simp_tac 3);
-by (res_inst_tac [("x", "xc")] bexI 3);
+by (res_inst_tac [("x", "K")] bexI 3);
 by (ALLGOALS(asm_simp_tac (simpset() 
     addsimps [FiniteFun_iff_multiset_on, multiset_on_def])));
 by Auto_tac;
@@ -836,7 +836,7 @@
 by (res_inst_tac [("x", "xb")] bexI 1);
 by (ALLGOALS(asm_full_simp_tac (simpset() 
     addsimps [FiniteFun_iff_multiset_on, multiset_on_def])));
-by (res_inst_tac [("x", "xc")] bexI 1);
+by (res_inst_tac [("x", "K")] bexI 1);
 by (ALLGOALS(asm_full_simp_tac (simpset() 
     addsimps [FiniteFun_iff_multiset_on,multiset_on_def])));
 by Auto_tac;

--- a/src/ZF/Integ/Bin.ML	Sun Nov 11 21:38:54 2001 +0100
+++ b/src/ZF/Integ/Bin.ML	Mon Nov 12 10:37:36 2001 +0100
@@ -348,7 +348,7 @@
 by (ALLGOALS (asm_full_simp_tac 
 	      (simpset() addsimps zcompare_rls @ 
 			  [zminus_zadd_distrib RS sym, int_of_add RS sym])));
-by (subgoal_tac "znegative ($- $# succ(x)) <-> znegative ($# succ(x))" 1);
+by (subgoal_tac "znegative ($- $# succ(n)) <-> znegative ($# succ(n))" 1);
 by (Asm_simp_tac 2);
 by (Full_simp_tac 1);
 qed "iszero_integ_of_BIT"; 
@@ -391,7 +391,7 @@
 by (ALLGOALS (asm_full_simp_tac 
 	      (simpset() addsimps [zminus_zadd_distrib RS sym, zdiff_def,
 				   int_of_add RS sym])));
-by (subgoal_tac "$#1 $- $# succ(succ(x #+ x)) = $- $# succ(x #+ x)" 1);
+by (subgoal_tac "$#1 $- $# succ(succ(n #+ n)) = $- $# succ(n #+ n)" 1);
 by (asm_full_simp_tac (simpset() addsimps [zdiff_def])1);
 by (asm_simp_tac (simpset() addsimps [equation_zminus, int_of_diff RS sym])1);
 qed "neg_integ_of_BIT"; 

--- a/src/ZF/Order.ML	Sun Nov 11 21:38:54 2001 +0100
+++ b/src/ZF/Order.ML	Mon Nov 12 10:37:36 2001 +0100
@@ -496,7 +496,7 @@
 \                     range(ord_iso_map(A,r,B,s)), s)";
 by (asm_simp_tac (simpset() addsimps [ord_iso_map_fun]) 1);
 by Safe_tac;
-by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1);
+by (subgoals_tac ["x:A", "ya:A", "y:B", "yb:B"] 1);
 by (REPEAT 
     (blast_tac (claset() addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
 by (asm_simp_tac 

--- a/src/ZF/Resid/Substitution.ML	Sun Nov 11 21:38:54 2001 +0100
+++ b/src/ZF/Resid/Substitution.ML	Mon Nov 12 10:37:36 2001 +0100
@@ -127,7 +127,7 @@
 by (etac redexes.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by Safe_tac;
-by (case_tac "n < xa" 1);
+by (case_tac "n < i" 1);
 by ((ftac lt_trans2 1) THEN (assume_tac 1));
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
 qed "lift_lift_rec";
@@ -187,7 +187,7 @@
 \       \\<forall>n \\<in> nat. \\<forall>v \\<in> redexes. subst_rec(v,lift_rec(u,n),n) =  u";
 by (etac redexes.induct 1);
 by Auto_tac;
-by (case_tac "n < x" 1);
+by (case_tac "n < na" 1);
 by Auto_tac;
 qed "subst_rec_lift_rec";
 

--- a/src/ZF/UNITY/Constrains.ML	Sun Nov 11 21:38:54 2001 +0100
+++ b/src/ZF/UNITY/Constrains.ML	Mon Nov 12 10:37:36 2001 +0100
@@ -524,25 +524,25 @@
 by (asm_full_simp_tac (simpset() addsimps [INT_iff,condition_def, mono_map_def]) 1);
 by (auto_tac (claset() addIs [comp_fun], simpset() addsimps [mono_map_def]));
 by (force_tac (claset() addSDs [bspec, ActsD],  simpset()) 1);
-by (subgoal_tac "xd:state" 1);
+by (subgoal_tac "xc:state" 1);
 by (blast_tac (claset() addSDs [ActsD]) 2);
-by (subgoal_tac "f`xe:A & f`xd:A" 1);
+by (subgoal_tac "f`xd:A & f`xc:A" 1);
 by (blast_tac (claset() addDs [apply_type]) 2);
 by (rotate_tac 3 1);
-by (dres_inst_tac [("x", "f`xe")] bspec 1);
+by (dres_inst_tac [("x", "f`xd")] bspec 1);
 by (Asm_simp_tac 1);
 by (REPEAT(etac conjE 1));
 by (rotate_tac ~3 1);
-by (dres_inst_tac [("x", "xc")] bspec 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
 by (Asm_simp_tac 1);
-by (dres_inst_tac [("c", "xd")] subsetD 1);
+by (dres_inst_tac [("c", "xc")] subsetD 1);
 by (rtac imageI 1);
 by Auto_tac;
 by (asm_full_simp_tac (simpset() addsimps [refl_def]) 1);
-by (dres_inst_tac [("x", "f`xe")] bspec 1);
-by (dres_inst_tac [("x", "f`xd")] bspec 2);
+by (dres_inst_tac [("x", "f`xd")] bspec 1);
+by (dres_inst_tac [("x", "f`xc")] bspec 2);
 by (ALLGOALS(Asm_simp_tac));
-by (dres_inst_tac [("b", "g`(f`xe)")] trans_onD 1);
+by (dres_inst_tac [("b", "g`(f`xd)")] trans_onD 1);
 by Auto_tac;
 qed "mono_Increasing_on_comp";
 

--- a/src/ZF/UNITY/Guar.ML	Sun Nov 11 21:38:54 2001 +0100
+++ b/src/ZF/UNITY/Guar.ML	Mon Nov 12 10:37:36 2001 +0100
@@ -129,7 +129,7 @@
 \ --> (JN G:GG. G):X)  --> uv_prop(X)";
 by Auto_tac;
 by (Clarify_tac 2);
-by (dres_inst_tac [("x", "{x,xa}")] spec 2);
+by (dres_inst_tac [("x", "{F,G}")] spec 2);
 by (dres_inst_tac [("x", "0")] spec 1);
 by (auto_tac (claset() addDs [ok_sym], 
     simpset() addsimps [OK_iff_ok]));

--- a/src/ZF/UNITY/UNITY.ML	Sun Nov 11 21:38:54 2001 +0100
+++ b/src/ZF/UNITY/UNITY.ML	Mon Nov 12 10:37:36 2001 +0100
@@ -550,7 +550,7 @@
 Goalw [constrains_def]
     "[| F : A co B; F : B co C |] ==> F : A co C";
 by Auto_tac;
-by (dres_inst_tac [("x", "x")] bspec 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
 by (dres_inst_tac [("x", "Id")] bspec 2);
 by (auto_tac (claset() addDs [ActsD], 
               simpset() addsimps [condition_def]));
@@ -560,7 +560,7 @@
    "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')";
 by Auto_tac;
 by (dres_inst_tac [("x", "Id")] bspec 1);
-by (dres_inst_tac [("x", "x")] bspec 2);
+by (dres_inst_tac [("x", "act")] bspec 2);
 by (auto_tac (claset(), simpset() addsimps [condition_def]));
 qed "constrains_cancel";
 
@@ -756,25 +756,25 @@
 by (asm_full_simp_tac (simpset() addsimps [INT_iff,condition_def, mono_map_def]) 1);
 by (auto_tac (claset() addIs [comp_fun], simpset() addsimps [mono_map_def]));
 by (force_tac (claset() addSDs [bspec, ActsD],  simpset()) 1);
-by (subgoal_tac "xd:state" 1);
+by (subgoal_tac "xc:state" 1);
 by (force_tac (claset() addSDs [ActsD], simpset()) 2);
-by (subgoal_tac "f`xe:A & f`xd:A" 1);
+by (subgoal_tac "f`xd:A & f`xc:A" 1);
 by (blast_tac (claset() addDs [apply_type]) 2);
 by (rotate_tac 3 1);
-by (dres_inst_tac [("x", "f`xe")] bspec 1);
+by (dres_inst_tac [("x", "f`xd")] bspec 1);
 by (Asm_simp_tac 1);
 by (REPEAT(etac conjE 1));
 by (rotate_tac ~2 1);
-by (dres_inst_tac [("x", "xc")] bspec 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
 by (Asm_simp_tac 1);
-by (dres_inst_tac [("c", "xd")] subsetD 1);
+by (dres_inst_tac [("c", "xc")] subsetD 1);
 by (rtac imageI 1);
 by Auto_tac;
 by (asm_full_simp_tac (simpset() addsimps [refl_def]) 1);
-by (dres_inst_tac [("x", "f`xe")] bspec 1);
-by (dres_inst_tac [("x", "f`xd")] bspec 2);
+by (dres_inst_tac [("x", "f`xd")] bspec 1);
+by (dres_inst_tac [("x", "f`xc")] bspec 2);
 by (ALLGOALS(Asm_simp_tac));
-by (dres_inst_tac [("b", "g`(f`xe)")] trans_onD 1);
+by (dres_inst_tac [("b", "g`(f`xd)")] trans_onD 1);
 by Auto_tac;
 qed "mono_increasing_on_comp";