proper handling of defs;

--- a/TFL/post.sml	Fri Aug 18 17:53:49 2000 +0200
+++ b/TFL/post.sml	Fri Aug 18 17:58:33 2000 +0200
@@ -185,11 +185,8 @@
  (*Strip off the outer !P*)
  val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
 
- fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
-    let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy)))
-			 ("Recursive definition " ^ id ^ 
-			  " would clash with the theory of the same name!")	(* FIXME !? *)
-	val def = freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
+ fun simplify_defn thy (ss, tflCongs) id pats def0 =
+    let	val def = freezeT def0 RS meta_eq_to_obj_eq
 	val {theory,rules,rows,TCs,full_pats_TCs} = 
 		 Prim.post_definition (Prim.congs thy tflCongs)
 		    (thy, (def,pats))
@@ -216,9 +213,8 @@
  *---------------------------------------------------------------------------*)
  fun define_i thy fid R ss_congs eqs = 
    let val {functional,pats} = Prim.mk_functional thy eqs
-       val thy = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
-   in (thy, simplify_defn ss_congs (thy, (fid, pats)))
-   end;
+       val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
+   in (thy, simplify_defn thy ss_congs fid pats def) end;
 
  fun define thy fid R ss_congs seqs = 
    define_i thy fid (read_term thy R) ss_congs (map (read_term thy) seqs)

--- a/TFL/tfl.sig	Fri Aug 18 17:53:49 2000 +0200
+++ b/TFL/tfl.sig	Fri Aug 18 17:58:33 2000 +0200
@@ -25,7 +25,7 @@
                        -> {functional:term,
                            pats: pattern list}
 
-   val wfrec_definition0 : theory -> string -> term -> term -> theory
+   val wfrec_definition0 : theory -> string -> term -> term -> theory * thm
 
    val post_definition : thm list -> theory * (thm * pattern list)
 				  -> {theory : theory,

--- a/TFL/tfl.sml	Fri Aug 18 17:53:49 2000 +0200
+++ b/TFL/tfl.sml	Fri Aug 18 17:58:33 2000 +0200
@@ -439,7 +439,8 @@
                           (wfrec $ map_term_types poly_tvars R)
                       $ functional
      val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
-  in  #1 (PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy)  end
+     val (thy', [def]) = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
+ in (thy', def) end;
 end;