# HG changeset patch
# User wenzelm
# Date 925488538 -7200
# Node ID 5be3f13193d72b82da87a313a12e790cb26a592f
# Parent  dc962d157a6309aad08d06801e9181bb36d4c302
tuned defer_recdef interfaces;

diff -r dc962d157a63 -r 5be3f13193d7 TFL/post.sml
--- a/TFL/post.sml	Fri Apr 30 18:07:19 1999 +0200
+++ b/TFL/post.sml	Fri Apr 30 18:08:58 1999 +0200
@@ -19,17 +19,17 @@
                            -> {induction:thm, rules:thm, TCs:term list list} 
                            -> {induction:thm, rules:thm, nested_tcs:thm list}
 
-   val define_i : theory -> xstring -> term -> term list
+   val define_i : theory -> string -> term -> term list
                   -> theory * Prim.pattern list
 
-   val define   : theory -> xstring -> string -> string list 
+   val define   : theory -> string -> string -> string list
                   -> theory * Prim.pattern list
 
-   val function_i : theory -> xstring 
+   val defer_i : theory -> string
                   -> thm list (* congruence rules *)
                   -> term list -> theory * thm
 
-   val function : theory -> xstring 
+   val defer : theory -> string
                   -> thm list 
                   -> string list -> theory * thm
 
@@ -241,10 +241,9 @@
    #1(strip_comb(#lhs(dest_eq(#2 (strip_forall(#2(strip_imp tm)))))))
  end;
 
- fun function_i thy fid congs eqs = 
-  let val dum = Theory.requires thy "WF_Rel" "recursive function definitions"
-      val {rules,R,theory,full_pats_TCs,SV,...} = 
-	      Prim.lazyR_def thy fid congs eqs
+ fun defer_i thy fid congs eqs = 
+  let val {rules,R,theory,full_pats_TCs,SV,...} = 
+	      Prim.lazyR_def thy (Sign.base_name fid) congs eqs
       val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
       val dummy = (message "Definition made."; message "Proving induction theorem ...");
       val induction = Prim.mk_induction theory 
@@ -256,10 +255,9 @@
       standard (induction RS (rules RS conjI)))
   end
 
- fun function thy fid congs seqs = 
-   let val _ =  message ("Deferred recursive function " ^ fid)
-       fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 
-   in  function_i thy fid congs (map (read thy) seqs)  end
+ fun defer thy fid congs seqs = 
+   let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[]))
+   in  defer_i thy fid congs (map (read thy) seqs)  end
    handle Utils.ERR {mesg,...} => error mesg;
 
  end;