author | clasohm |
Wed, 29 Jun 1994 12:13:03 +0200 | |
changeset 443 | 10884e64c241 |
parent 442 | 13ac1fd0a14d |
child 444 | 3ca9d49fd662 |
src/ZF/WF.ML | file | annotate | diff | comparison | revisions |
--- a/src/ZF/WF.ML Wed Jun 29 12:03:41 1994 +0200 +++ b/src/ZF/WF.ML Wed Jun 29 12:13:03 1994 +0200 @@ -217,7 +217,7 @@ 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();