diff -r 5ff4bfab859c -r 112cbb8301dc TFL/tfl.sig
--- a/TFL/tfl.sig	Mon Jun 23 11:30:35 1997 +0200
+++ b/TFL/tfl.sig	Mon Jun 23 11:33:59 1997 +0200
@@ -17,7 +17,7 @@
 
    val wfrec_definition0 : theory -> string -> term -> term -> theory
 
-   val post_definition : simpset -> theory * (thm * pattern list)
+   val post_definition : simpset * thm list -> theory * (thm * pattern list)
 				 -> {theory : theory,
 				     rules  : thm, 
 				       TCs  : term list list,
@@ -25,7 +25,7 @@
 				  patterns  : pattern list}
 
 (*CURRENTLY UNUSED
-   val wfrec_eqns : theory -> term list
+   val wfrec_eqns : simpset * thm list -> theory -> term list
                      -> {WFR : term, 
                          proto_def : term,
                          extracta :(thm * term list) list,
@@ -46,10 +46,4 @@
                      -> theory 
                       -> {rules:thm, induction:thm, TCs:term list list}
                        -> {rules:thm, induction:thm, nested_tcs:thm list}
-
-   structure Context
-     : sig
-         val read : unit -> thm list
-         val write : thm list -> unit
-       end
 end;