--- a/TFL/post.sml Wed May 27 12:19:35 1998 +0200
+++ b/TFL/post.sml Wed May 27 12:21:39 1998 +0200
@@ -84,7 +84,7 @@
* Defining a function with an associated termination relation.
*---------------------------------------------------------------------------*)
fun define_i thy fid R eqs =
- let val dummy = Theory.require thy "WF_Rel" "recursive function definitions"
+ let val dummy = Theory.requires thy "WF_Rel" "recursive function definitions"
val {functional,pats} = Prim.mk_functional thy eqs
in (Prim.wfrec_definition0 thy fid R functional, pats)
end;