# HG changeset patch # User wenzelm # Date 924778140 -7200 # Node ID 92d142e58a5bc7e14704c423a3a3eddc3a3861f0 # Parent 19e005e2f58d8f141771d4e67df87be83df4d52a Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML; Sign.base_name fid; diff -r 19e005e2f58d -r 92d142e58a5b TFL/post.sml --- 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"