TFL/usyntax.sml
changeset 10212 33fe2d701ddd
parent 10117 8e58b3045e29
     1.1 --- a/TFL/usyntax.sml	Thu Oct 12 18:09:06 2000 +0200
     1.2 +++ b/TFL/usyntax.sml	Thu Oct 12 18:38:23 2000 +0200
     1.3 @@ -407,7 +407,7 @@
     1.4                                    mesg="unexpected term structure"} (* FIXME do not handle _ !!! *)
     1.5     else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
     1.6  
     1.7 -fun is_WFR (Const("WF.wf",_)$_) = true
     1.8 +fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true
     1.9    | is_WFR _                 = false;
    1.10  
    1.11  fun ARB ty = mk_select{Bvar=Free("v",ty),