# HG changeset patch
# User paulson
# Date 1151597475 -7200
# Node ID 73704ba4bed1351671636e6fcd5ff11cf27a07a9
# Parent  806eaa2a2a5e6ea67f0bfdfe7b6b242bacab0ecb
added the "th" field to datatype Clause

diff -r 806eaa2a2a5e -r 73704ba4bed1 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Thu Jun 29 18:10:59 2006 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Thu Jun 29 18:11:15 2006 +0200
@@ -204,6 +204,7 @@
 datatype clause = 
 	 Clause of {clause_id: clause_id,
 		    axiom_name: axiom_name,
+		    th: thm,
 		    kind: kind,
 		    literals: literal list,
 		    ctypes_sorts: (ctyp_var * csort) list, 
@@ -281,11 +282,12 @@
 
 
 
-fun make_clause(clause_id,axiom_name,kind,literals,ctypes_sorts,ctvar_type_literals,ctfree_type_literals) =
+fun make_clause(clause_id,axiom_name,th,kind,literals,ctypes_sorts,ctvar_type_literals,ctfree_type_literals) =
     if forall isFalse literals
     then error "Problem too trivial for resolution (empty clause)"
     else
-	Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind,
+	Clause {clause_id = clause_id, axiom_name = axiom_name, 
+                th = th, kind = kind, 
 		literals = literals, ctypes_sorts = ctypes_sorts, 
 		ctvar_type_literals = ctvar_type_literals,
 		ctfree_type_literals = ctfree_type_literals};
@@ -466,12 +468,11 @@
 (* making axiom and conjecture clauses *)
 fun make_axiom_clause thm (ax_name,cls_id) =
     let val term = prop_of thm
-	val term' = comb_of term
-	val (lits,ctypes_sorts) = literals_of_term term'
+	val (lits,ctypes_sorts) = literals_of_term (comb_of term)
 	val lits' = sort_lits lits
 	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
     in
-	make_clause(cls_id,ax_name,Axiom,
+	make_clause(cls_id,ax_name,thm,Axiom,
 		    lits',ctypes_sorts,ctvar_lits,ctfree_lits)
     end;
 
@@ -486,11 +487,10 @@
 
 fun make_conjecture_clause n thm =
     let val t = prop_of thm
-	val t' = comb_of t
-	val (lits,ctypes_sorts) = literals_of_term t'
+	val (lits,ctypes_sorts) = literals_of_term (comb_of t)
 	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
     in
-	make_clause(n,"conjecture",Conjecture,lits,ctypes_sorts,ctvar_lits,ctfree_lits)
+	make_clause(n,"conjecture",thm,Conjecture,lits,ctypes_sorts,ctvar_lits,ctfree_lits)
     end;