src/HOL/Tools/ATP/res_clasimpset.ML

 
   val relevant : int ref
   val use_simpset: bool ref
   val use_nameless: bool ref
   val write_out_clasimp : string -> theory -> term -> 
-                             (ResClause.clause * thm) Array.array * int (* * ResClause.clause list *)
+                             (ResClause.clause * thm) Array.array * int * ResClause.clause list 
 
   end;
 
 structure ResClasimp : RES_CLASIMP =
 struct

 	val out = TextIO.openOut filename;
 	val _=   ResLib.writeln_strs out stick_clasrls;
 	val _= TextIO.flushOut out;
 	val _= TextIO.closeOut out
   in
-	(clause_arr, num_of_clauses)
+	(clause_arr, num_of_clauses, clauses)
   end;
 
 
 end;