WF.ML

--- a/WF.ML	Mon Jun 20 14:52:40 1994 +0200
+++ b/WF.ML	Fri Jun 24 15:10:13 1994 +0200
@@ -42,10 +42,10 @@
 by (fast_tac (HOL_cs addIs prems) 1);
 by (wf_ind_tac "a" prems 1);
 by (fast_tac set_cs 1);
-val wf_anti_sym = result();
+val wf_asym = result();
 
 val prems = goal WF.thy "[| wf(r);  <a,a>: r |] ==> P";
-by (rtac wf_anti_sym 1);
+by (rtac wf_asym 1);
 by (REPEAT (resolve_tac prems 1));
 val wf_anti_refl = result();