src/HOL/WF.ML
changeset 1786 8a31d85d27b8
parent 1771 ee81183a77a0
child 2031 03a843f0f447
--- a/src/HOL/WF.ML	Mon Jun 03 11:44:44 1996 +0200
+++ b/src/HOL/WF.ML	Mon Jun 03 17:10:56 1996 +0200
@@ -19,7 +19,7 @@
 by (strip_tac 1);
 by (rtac allE 1);
 by (assume_tac 1);
-by (best_tac (HOL_cs addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
+by (best_tac (!claset addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
 qed "wfI";
 
 val major::prems = goalw WF.thy [wf_def]