# HG changeset patch
# User paulson
# Date 953727837 -3600
# Node ID 52ef986bd0a6c72cf352fed9a4c5f8d07889deeb
# Parent  17325ee838ab2e5be8561dfa0c8373dfbab2e806
made a proof more robust (did not like Suc_less_eq)

diff -r 17325ee838ab -r 52ef986bd0a6 src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Wed Mar 22 13:22:39 2000 +0100
+++ b/src/HOL/WF_Rel.ML	Wed Mar 22 13:23:57 2000 +0100
@@ -101,7 +101,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() addSIs [psubset_card]) 1);
+by (fast_tac (claset() addSEs [psubset_card]) 1);
 qed "wf_finite_psubset";
 
 Goalw [finite_psubset_def, trans_def] "trans finite_psubset";