diff -r 91a91790899a -r 2cccd0e3e9ea TFL/tfl.sig
--- a/TFL/tfl.sig	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/tfl.sig	Thu Jun 05 13:27:28 1997 +0200
@@ -15,23 +15,22 @@
                        -> {functional:term,
                            pats: pattern list}
 
-   val wfrec_definition0 : theory -> string -> term -> term -> thm * theory
+   val wfrec_definition0 : theory -> string -> term -> term -> theory
 
-   val post_definition : theory * (thm * pattern list)
-                              -> {theory : theory,
-                                  rules  : thm, 
-                                    TCs  : term list list,
-                          full_pats_TCs  : (term * term list) list, 
-                               patterns  : pattern list}
+   val post_definition : simpset -> theory * (thm * pattern list)
+				 -> {theory : theory,
+				     rules  : thm, 
+				       TCs  : term list list,
+			     full_pats_TCs  : (term * term list) list, 
+				  patterns  : pattern list}
 
-
+(*CURRENTLY UNUSED
    val wfrec_eqns : theory -> term list
                      -> {WFR : term, 
                          proto_def : term,
                          extracta :(thm * term list) list,
                          pats  : pattern list}
 
-
    val lazyR_def : theory
                    -> term list
                    -> {theory:theory,
@@ -39,11 +38,9 @@
                            R :term,
                        full_pats_TCs :(term * term list) list, 
                        patterns: pattern list}
+---------------------*)
 
-   val mk_induction : theory 
-                       -> term -> term 
-                         -> (term * term list) list
-                           -> thm
+   val mk_induction : theory -> term -> term -> (term * term list) list -> thm
 
    val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
                      -> theory