--- a/src/HOL/NumberTheory/IntFact.ML Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/NumberTheory/IntFact.ML Wed Aug 30 10:21:19 2000 +0200
@@ -60,7 +60,7 @@
qed "d22set_le_swap";
Goal "#1<b --> b<=a --> b:(d22set a)";
-by (res_inst_tac [("u","a")] d22set.induct 1);
+by (res_inst_tac [("x","a")] d22set.induct 1);
by Auto_tac;
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq])));
qed_spec_mp "d22set_mem";
@@ -75,7 +75,7 @@
Delsimps zfact.simps;
Goal "setprod(d22set a) = zfact a";
-by (res_inst_tac [("u","a")] d22set.induct 1);
+by (res_inst_tac [("x","a")] d22set.induct 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 1);
by (stac d22set_eq 1);