# HG changeset patch
# User paulson
# Date 865246377 -7200
# Node ID 8db8fc8607d917259d21bf9984f50198253277d6
# Parent  2bac33ec2b0d11c2dde071add11e61b2abb8353a
Simplified proof

diff -r 2bac33ec2b0d -r 8db8fc8607d9 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon Jun 02 12:12:27 1997 +0200
+++ b/src/HOL/Finite.ML	Mon Jun 02 12:12:57 1997 +0200
@@ -62,7 +62,7 @@
 
 goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
 by (stac insert_is_Un 1);
-by (Simp_tac 1);
+by (simp_tac (HOL_ss addsimps [subset_Fin]) 1);
 by (blast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
 qed "insert_Fin";
 Addsimps[insert_Fin];