Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML;
authorwenzelm
Thu, 22 Apr 1999 12:49:00 +0200
changeset 6476 92d142e58a5b
parent 6475 19e005e2f58d
child 6477 e36581d04eee
Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML; Sign.base_name fid;
TFL/post.sml file | annotate | diff | comparison | revisions 
--- 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"
isabelle