# HG changeset patch
# User clasohm
# Date 772884783 -7200
# Node ID 10884e64c241e7dbc4edaff00d6bd3a61a2f3303
# Parent  13ac1fd0a14dc97447629b9feaa4e514779b4d3a
added parentheses made necessary by new constrain precedence

diff -r 13ac1fd0a14d -r 10884e64c241 src/ZF/WF.ML
--- 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();