src/CCL/genrec.ML

 \       !!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==>\
 \               h(p,g) : D(p) |] ==> \
 \    letrec g x be h(x,g) in g(a) : D(a)";
 by (rtac (major RS rev_mp) 1);
 by (rtac (wf_wf RS wfd_induct) 1);
-by (rtac (letrecB RS ssubst) 1);
+by (stac letrecB 1);
 by (rtac impI 1);
 by (eresolve_tac prems 1);
 by (rtac ballI 1);
 by (etac (spec RS mp RS mp) 1);
 by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1));

 \             ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
 \               h(p,q,g) : D(p,q) |] ==> \
 \    letrec g x y be h(x,y,g) in g(a,b) : D(a,b)";
 by (rtac (SPLITB RS subst) 1);
 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
-by (rtac (SPLITB RS ssubst) 1);
+by (stac SPLITB 1);
 by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
 by (rtac (SPLITB RS subst) 1);
 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
             eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
 qed "letrec2T";