src/HOL/WF_Rel.ML

--- a/src/HOL/WF_Rel.ML	Tue Jul 01 17:59:36 1997 +0200
+++ b/src/HOL/WF_Rel.ML	Wed Jul 02 11:59:10 1997 +0200
@@ -92,7 +92,7 @@
 by (rtac (wf_measure RS wf_subset) 1);
 by (simp_tac (!simpset addsimps [measure_def, inv_image_def, less_than_def,
 				 symmetric less_def])1);
-by (fast_tac (!claset addIs [psubset_card]) 1);
+by (fast_tac (!claset addSIs [psubset_card]) 1);
 qed "wf_finite_psubset";
 
 goalw thy [finite_psubset_def, trans_def] "trans finite_psubset";