src/ZF/WF.ML

 by (assume_tac 1);
 val is_recfun_type = result();
 
 val [isrec,rel] = goalw WF.thy [is_recfun_def]
     "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";
-by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1);
+by (res_inst_tac [("P", "%x.?t(x) = (?u::i)")] (isrec RS ssubst) 1);
 by (rtac (rel RS underI RS beta) 1);
 val apply_recfun = result();
 
 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   spec RS mp  instantiates induction hypotheses*)