# HG changeset patch
# User paulson
# Date 864642510 -7200
# Node ID c81c7f8ad333e56730f80ef4794df3db29beb2ba
# Parent  ab7161e593c87eb60db858dfd885cb1bd3bc42a8
Now checks the name of the function being defined

diff -r ab7161e593c8 -r c81c7f8ad333 TFL/post.sml
--- a/TFL/post.sml	Mon May 26 12:27:58 1997 +0200
+++ b/TFL/post.sml	Mon May 26 12:28:30 1997 +0200
@@ -27,8 +27,11 @@
                            -> {induction:thm, rules:thm, TCs:term list list} 
                            -> {induction:thm, rules:thm, nested_tcs:thm list}
 
-   val define_i : theory -> term -> term -> theory * (thm * Prim.pattern list)
-   val define   : theory -> string -> string list -> theory * Prim.pattern list
+   val define_i : theory -> string -> term -> term 
+                  -> theory * (thm * Prim.pattern list)
+
+   val define   : theory -> string -> string -> string list 
+                  -> theory * Prim.pattern list
 
    val simplify_defn : theory * (string * Prim.pattern list)
                         -> {rules:thm list, induct:thm, tcs:term list}
@@ -74,9 +77,9 @@
   *--------------------------------------------------------------------------*)
  fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
  val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, 
-                    wf_pred_list, wf_trancl];
+                    wf_trancl];
 
- val terminator = simp_tac(!simpset addsimps [less_Suc_eq, pred_list_def]) 1
+ val terminator = simp_tac(!simpset addsimps [less_Suc_eq]) 1
                   THEN TRY(best_tac
                            (!claset addSDs [not0_implies_Suc]
                                     addss (!simpset)) 1);
@@ -105,20 +108,19 @@
 (*---------------------------------------------------------------------------
  * Defining a function with an associated termination relation. 
  *---------------------------------------------------------------------------*)
-fun define_i thy R eqs = 
-  let val dummy = require_thy thy "WF_Rel" "recursive function definitions";
-      
+fun define_i thy fid R eqs = 
+  let val dummy = require_thy thy "WF_Rel" "recursive function definitions"
       val {functional,pats} = Prim.mk_functional thy eqs
-      val (thm,thry) = Prim.wfrec_definition0 thy  R functional
+      val (thm,thry) = Prim.wfrec_definition0 thy fid R functional
   in (thry,(thm,pats))
   end;
 
 (*lcp's version: takes strings; doesn't return "thm" 
         (whose signature is a draft and therefore useless) *)
-fun define thy R eqs = 
+fun define thy fid R eqs = 
   let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) 
       val (thy',(_,pats)) =
-             define_i thy (read thy R) 
+             define_i thy fid (read thy R) 
                       (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs))
   in  (thy',pats)  end
   handle Utils.ERR {mesg,...} => error mesg;