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.
Sign.base_name fid;
authorwenzelm
Fri, 16 Apr 1999 14:43:26 +0200
changeset 6436 90eab99706e3
parent 6435 154b88d2b62e
child 6437 9bdfe07ba8e9
Sign.base_name fid;
TFL/post.sml file | annotate | diff | comparison | revisions 
--- a/TFL/post.sml	Fri Apr 16 14:42:44 1999 +0200
+++ b/TFL/post.sml	Fri Apr 16 14:43:26 1999 +0200
@@ -95,11 +95,10 @@
 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)
+  in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats)
   end;
 
-(*lcp's version: takes strings; doesn't return "thm" 
-        (whose signature is a draft and therefore useless) *)
+(*lcp's version: takes strings; doesn't return "thm"*)
 fun define thy fid R eqs = 
   let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 
   in  define_i thy fid (read thy R) (map (read thy) eqs)  end
isabelle