diff -r 11f4884a071a -r 7091ffa99c93 TFL/rules.sig
--- a/TFL/rules.sig	Fri May 30 15:30:52 1997 +0200
+++ b/TFL/rules.sig	Fri May 30 15:55:27 1997 +0200
@@ -50,14 +50,12 @@
   val simpl_conv : thm list -> cterm -> thm
 
 (* For debugging my isabelle solver in the conditional rewriter *)
-(*
   val term_ref : term list ref
   val thm_ref : thm list ref
   val mss_ref : meta_simpset list ref
   val tracing :bool ref
-*)
   val CONTEXT_REWRITE_RULE : term * term
-                             -> {thms:thm list,congs: thm list, th:thm} 
+                             -> {cut_lemma:thm, congs: thm list, th:thm} 
                              -> thm * term list
   val RIGHT_ASSOC : thm -> thm