1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Apr 19 10:42:13 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Apr 19 10:42:45 2006 +0200
     1.3 @@ -233,6 +233,7 @@
     1.4  datatype clause = 
     1.5  	 Clause of {clause_id: clause_id,
     1.6  		    axiom_name: axiom_name,
     1.7 +		    th: thm,
     1.8  		    kind: kind,
     1.9  		    literals: literal list,
    1.10  		    types_sorts: (typ_var * sort) list};
    1.11 @@ -253,11 +254,12 @@
    1.12    
    1.13  fun isTaut (Clause {literals,...}) = exists isTrue literals;  
    1.14  
    1.15 -fun make_clause (clause_id, axiom_name, kind, literals, types_sorts) =
    1.16 +fun make_clause (clause_id, axiom_name, th, kind, literals, types_sorts) =
    1.17    if forall isFalse literals 
    1.18    then error "Problem too trivial for resolution (empty clause)"
    1.19    else
    1.20 -     Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, 
    1.21 +     Clause {clause_id = clause_id, axiom_name = axiom_name, 
    1.22 +             th = th, kind = kind, 
    1.23               literals = literals, types_sorts = types_sorts};
    1.24  
    1.25  
    1.26 @@ -576,7 +578,7 @@
    1.27  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t)
    1.28  	val (lits,types_sorts) = literals_of_term t
    1.29      in
    1.30 -	make_clause(n, "conjecture", Conjecture, lits, types_sorts)
    1.31 +	make_clause(n, "conjecture", thm, Conjecture, lits, types_sorts)
    1.32      end;
    1.33      
    1.34  fun make_conjecture_clauses_aux _ [] = []
    1.35 @@ -612,7 +614,7 @@
    1.36  	else if forall too_general_lit lits then
    1.37  	   (Output.debug ("Omitting " ^ ax_name ^ ": equalities are too general"); 
    1.38  	    NONE)
    1.39 -	else SOME (make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts))
    1.40 +	else SOME (make_clause(cls_id, ax_name, thm, Axiom, sort_lits lits, types_sorts))
    1.41      end
    1.42      handle CLAUSE _ => NONE;
    1.43