added parentheses made necessary by new constrain precedence
authorclasohm
Wed Jun 29 12:13:03 1994 +0200 (1994-06-29 ago)
changeset 44310884e64c241
parent 442 13ac1fd0a14d
child 444 3ca9d49fd662
added parentheses made necessary by new constrain precedence
src/ZF/WF.ML
     1.1 --- a/src/ZF/WF.ML	Wed Jun 29 12:03:41 1994 +0200
     1.2 +++ b/src/ZF/WF.ML	Wed Jun 29 12:13:03 1994 +0200
     1.3 @@ -217,7 +217,7 @@
     1.4  
     1.5  val [isrec,rel] = goalw WF.thy [is_recfun_def]
     1.6      "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";
     1.7 -by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1);
     1.8 +by (res_inst_tac [("P", "%x.?t(x) = (?u::i)")] (isrec RS ssubst) 1);
     1.9  by (rtac (rel RS underI RS beta) 1);
    1.10  val apply_recfun = result();
    1.11