# HG changeset patch
# User wenzelm
# Date 924266606 -7200
# Node ID 90eab99706e3d8bd89e88e70a3748d358a8b1d72
# Parent  154b88d2b62eaa18dcacba9153f738b1e8a06eeb
Sign.base_name fid;

diff -r 154b88d2b62e -r 90eab99706e3 TFL/post.sml
--- 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