# HG changeset patch
# User nipkow
# Date 855321238 -3600
# Node ID 3b4ad6c7726fe75f9b44c6729313d67a05e695c4
# Parent  548f8ed89a807925620341ef1360e6f92cc73c56
Modified proofs because of added "triv_forall_equality".

diff -r 548f8ed89a80 -r 3b4ad6c7726f src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Fri Feb 07 14:13:20 1997 +0100
+++ b/src/HOL/Integ/Integ.ML	Fri Feb 07 14:13:58 1997 +0100
@@ -577,11 +577,12 @@
 by (safe_tac (!claset));
 by (asm_full_simp_tac (!simpset addsimps [zadd, zminus]) 1);
 by (safe_tac (!claset addSDs [less_eq_Suc_add]));
+by (rename_tac "k" 1);
 by (res_inst_tac [("x","k")] exI 1);
 by (asm_full_simp_tac (!simpset delsimps [add_Suc, add_Suc_right]
                                 addsimps ([add_Suc RS sym] @ add_ac)) 1);
 (*To cancel x2, rename it to be first!*)
-by (rename_tac "a b c" 1);
+by (rename_tac "a b" 1);
 by (asm_full_simp_tac (!simpset delsimps [add_Suc_right]
                                 addsimps (add_left_cancel::add_ac)) 1);
 qed "zless_eq_zadd_Suc";
diff -r 548f8ed89a80 -r 3b4ad6c7726f src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Fri Feb 07 14:13:20 1997 +0100
+++ b/src/HOL/W0/W.ML	Fri Feb 07 14:13:58 1997 +0100
@@ -219,7 +219,6 @@
 		     addss !simpset) 1); 
 qed_spec_mp "free_tv_W"; 
 
-
 (* Completeness of W w.r.t. has_type *)
 goal thy
  "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
@@ -347,9 +346,8 @@
 by (rtac conjI 1);
 by (dres_inst_tac [("x","ma")] fun_cong 2);
 by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
-by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
-by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
-    (2,trans)) 1);
+by (simp_tac (!simpset addsimps [o_def,subst_comp_tel RS sym]) 1);
+by (rtac ((subst_comp_tel RS sym) RSN (2,trans)) 1);
 by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
 (** LEVEL 90 **)
 by (rtac eq_free_eq_subst_tel 1);
diff -r 548f8ed89a80 -r 3b4ad6c7726f src/HOL/ex/LList.ML
--- a/src/HOL/ex/LList.ML	Fri Feb 07 14:13:20 1997 +0100
+++ b/src/HOL/ex/LList.ML	Fri Feb 07 14:13:58 1997 +0100
@@ -297,15 +297,19 @@
 \    !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
 \ ==> h1=h2";
 by (rtac (ntrunc_equality RS ext) 1);
+by (rename_tac "x k" 1);
 by (res_inst_tac [("x", "x")] spec 1);
 by (res_inst_tac [("n", "k")] less_induct 1);
+by (rename_tac "n" 1);
 by (rtac allI 1);
+by (rename_tac "y" 1);
 by (stac prem1 1);
 by (stac prem2 1);
 by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
 by (strip_tac 1);
 by (res_inst_tac [("n", "n")] natE 1);
-by (res_inst_tac [("n", "xb")] natE 2);
+by (rename_tac "m" 2);
+by (res_inst_tac [("n", "m")] natE 2);
 by (ALLGOALS(asm_simp_tac(!simpset addsimps
             [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
 result();