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