# HG changeset patch
# User oheimb
# Date 905511340 -7200
# Node ID 1c09934fe445a1841d32e4432026128954b1200f
# Parent  410172655d64e22e6afaa54e7de6e88c58cd498d
corrected indentation

diff -r 410172655d64 -r 1c09934fe445 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Thu Sep 10 18:07:06 1998 +0200
+++ b/src/HOL/Finite.ML	Fri Sep 11 12:55:40 1998 +0200
@@ -325,7 +325,7 @@
 by (Clarify_tac 1);
 by (case_tac "x:B" 1);
  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
-by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
+ by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
 by (fast_tac (claset() addss
 	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);
 qed_spec_mp "card_mono";