# HG changeset patch
# User oheimb
# Date 982179899 -3600
# Node ID 0a258a048d8d3626bd8d83c6e361879c07a39caa
# Parent  44db3b518ca2b0db0bf47a65fc87b31cae886381
supressed some warnings on identical proofstate

diff -r 44db3b518ca2 -r 0a258a048d8d src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Wed Feb 14 19:31:05 2001 +0100
+++ b/src/HOL/Finite.ML	Wed Feb 14 20:44:59 2001 +0100
@@ -303,8 +303,7 @@
 Goal "(A,m): cardR ==> (ALL n. (A,n) : cardR --> n=m)";
 by (etac cardR.induct 1);
  by (safe_tac (claset() addSEs [cardR_insertE]));
-by (rename_tac "B b m" 1);
-by (case_tac "a = b" 1);
+by (rename_tac "B b m" 1 THEN case_tac "a = b" 1);
  by (subgoal_tac "A = B" 1);
   by (blast_tac (claset() addEs [equalityE]) 2);
  by (Blast_tac 1);
@@ -570,8 +569,7 @@
 by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
 by (rtac impI 1);
 (** LEVEL 10 **)
-by (rename_tac "Aa xa ya Ab xb yb" 1);
- by (case_tac "xa=xb" 1);
+by (rename_tac "Aa xa ya Ab xb yb" 1 THEN case_tac "xa=xb" 1);
  by (subgoal_tac "Aa = Ab" 1);
  by (blast_tac (claset() addSEs [equalityE]) 2);
  by (Blast_tac 1);