--- a/TFL/post.sml Thu Apr 22 12:47:13 1999 +0200
+++ b/TFL/post.sml Thu Apr 22 12:49:00 1999 +0200
@@ -84,9 +84,8 @@
* Defining a function with an associated termination relation.
*---------------------------------------------------------------------------*)
fun define_i thy fid R eqs =
- 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)
+ let val {functional,pats} = Prim.mk_functional thy eqs
+ in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats)
end;
(*lcp's version: takes strings; doesn't return "thm"