src/HOL/Tools/ATP/res_clasimpset.ML
changeset 17150 ce2a1aeb42aa
parent 16957 8dcd14e8db7a
child 17234 12a9393c5d77
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Aug 26 10:01:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Aug 26 19:36:07 2005 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4    val use_simpset: bool ref
     1.5    val use_nameless: bool ref
     1.6    val write_out_clasimp : string -> theory -> term -> 
     1.7 -                             (ResClause.clause * thm) Array.array * int (* * ResClause.clause list *)
     1.8 +                             (ResClause.clause * thm) Array.array * int * ResClause.clause list 
     1.9  
    1.10    end;
    1.11  
    1.12 @@ -245,7 +245,7 @@
    1.13  	val _= TextIO.flushOut out;
    1.14  	val _= TextIO.closeOut out
    1.15    in
    1.16 -	(clause_arr, num_of_clauses)
    1.17 +	(clause_arr, num_of_clauses, clauses)
    1.18    end;
    1.19  
    1.20