# HG changeset patch
# User paulson
# Date 961154355 -7200
# Node ID b8780970d0edcb237de3df9b303329a98a62a563
# Parent  5bf9b0d6df8ac99a7a2de92e2ba17621e7c96a31
tidied for new card_seteq

diff -r 5bf9b0d6df8a -r b8780970d0ed src/HOL/IMPP/Hoare.ML
--- a/src/HOL/IMPP/Hoare.ML	Fri Jun 16 13:18:55 2000 +0200
+++ b/src/HOL/IMPP/Hoare.ML	Fri Jun 16 13:19:15 2000 +0200
@@ -260,9 +260,8 @@
 by (cut_facts_tac (premises()) 1);
 by (induct_tac "n" 1);
 by  (ALLGOALS Clarsimp_tac);
-bd  card_seteq 1;
-by    (Asm_simp_tac 1);
-be   finite_imageI 1;
+by  (subgoal_tac "G = mgt_call `` U" 1);
+by   (asm_simp_tac (simpset() addsimps [card_seteq, finite_imageI]) 2);
 by  (Asm_full_simp_tac 1);
 by  (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
 br  ballI 1;