--- a/ex/Finite.ML	Tue Mar 22 08:31:58 1994 +0100
+++ b/ex/Finite.ML	Tue Mar 22 08:32:22 1994 +0100
@@ -86,8 +86,8 @@
 \    |] ==> c<=b --> P(b-c)";
 by (rtac (major RS Fin_induct) 1);
 by (rtac (Diff_insert RS ssubst) 2);
-by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[insert_subset_iff, 
-				Diff_subset RS Fin_subset]))));
+by (ALLGOALS (asm_simp_tac
+                (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
 val Fin_empty_induct_lemma = result();
 
 val prems = goal Finite.thy