# HG changeset patch
# User mengj
# Date 1141700661 -3600
# Node ID 1da6b9a1575dd5ee8eaf2159b87a7c2a0856ea8c
# Parent  b338c218cc6e125a1c0f762df2e52a6fc422f23f
relevance_filter takes input axioms as Term.term.

diff -r b338c218cc6e -r 1da6b9a1575d src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Mar 07 04:01:25 2006 +0100
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Mar 07 04:04:21 2006 +0100
@@ -75,11 +75,11 @@
 
 
 fun relevant_clauses_ax_g_1 _ []  _ (ax,r) = (ax,r)
-  | relevant_clauses_ax_g_1 gconsts  ((clsthm,(consts,_))::y) P (ax,r) =
+  | relevant_clauses_ax_g_1 gconsts  ((clstm,(consts,_))::y) P (ax,r) =
     let val weight = find_clause_weight_s_1 gconsts consts 1.0
     in
-	if  P <= weight then relevant_clauses_ax_g_1 gconsts y P ((clsthm,(consts,weight))::ax,r)
-	else relevant_clauses_ax_g_1 gconsts y P (ax,(clsthm,(consts,weight))::r)
+	if  P <= weight then relevant_clauses_ax_g_1 gconsts y P ((clstm,(consts,weight))::ax,r)
+	else relevant_clauses_ax_g_1 gconsts y P (ax,(clstm,(consts,weight))::r)
     end;
 
 
@@ -87,22 +87,21 @@
     (case addc of [] => rel_axs @ keep
 		| _ => case tmpc of [] => addc @ rel_axs @ keep
 				  | _ => relevant_clauses_ax_1 addc tmpc P ([],[]) (rel_axs @ keep))
-  | relevant_clauses_ax_1 rel_axs ((clsthm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
+  | relevant_clauses_ax_1 rel_axs ((clstm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
     let val weight' = find_clause_weight_m_1 rel_axs (consts,weight) 
-	val e_ax' = (clsthm,(consts, weight'))
+	val e_ax' = (clstm,(consts, weight'))
     in
 	
-	if P <= weight' then relevant_clauses_ax_1 rel_axs e_axs P ((clsthm,(consts,weight'))::addc,tmpc) keep
-	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clsthm,(consts,weight'))::tmpc) keep 
+	if P <= weight' then relevant_clauses_ax_1 rel_axs e_axs P ((clstm,(consts,weight'))::addc,tmpc) keep
+	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clstm,(consts,weight'))::tmpc) keep 
     end;
 
 
 fun initialize [] ax_weights = ax_weights
-  | initialize ((cls,thm)::clss_thms) ax_weights =
-    let val tm = prop_of thm
-	val consts = consts_of_term tm
+  | initialize ((tm,name)::tms_names) ax_weights =
+    let val consts = consts_of_term tm
     in
-	initialize clss_thms (((cls,thm),(consts,0.0))::ax_weights)
+	initialize tms_names (((tm,name),(consts,0.0))::ax_weights)
     end;
 
 fun relevance_filter1_aux axioms goals = 
@@ -139,11 +138,11 @@
 
 
 fun relevant_clauses_ax_g_2 _ []  _ (ax,r) = (ax,r)
-  | relevant_clauses_ax_g_2 gpconsts  ((clsthm,(pconsts,_))::y) P (ax,r) =
+  | relevant_clauses_ax_g_2 gpconsts  ((clstm,(pconsts,_))::y) P (ax,r) =
     let val weight = find_clause_weight_s_2 gpconsts pconsts 1.0
     in
-	if  P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clsthm,(pconsts,weight))::ax,r)
-	else relevant_clauses_ax_g_2 gpconsts y P (ax,(clsthm,(pconsts,weight))::r)
+	if  P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clstm,(pconsts,weight))::ax,r)
+	else relevant_clauses_ax_g_2 gpconsts y P (ax,(clstm,(pconsts,weight))::r)
     end;
 
 
@@ -151,22 +150,21 @@
     (case addc of [] => rel_axs @ keep
 		| _ => case tmpc of [] => addc @ rel_axs @ keep
 				  | _ => relevant_clauses_ax_2 addc tmpc P ([],[]) (rel_axs @ keep))
-  | relevant_clauses_ax_2 rel_axs ((clsthm,(pconsts,weight))::e_axs) P (addc,tmpc) keep = 
+  | relevant_clauses_ax_2 rel_axs ((clstm,(pconsts,weight))::e_axs) P (addc,tmpc) keep = 
     let val weight' = find_clause_weight_m_2 rel_axs (pconsts,weight) 
-	val e_ax' = (clsthm,(pconsts, weight'))
+	val e_ax' = (clstm,(pconsts, weight'))
     in
 	
-	if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clsthm,(pconsts,weight'))::addc,tmpc) keep
-	else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clsthm,(pconsts,weight'))::tmpc) keep 
+	if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clstm,(pconsts,weight'))::addc,tmpc) keep
+	else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clstm,(pconsts,weight'))::tmpc) keep 
     end;
 
 
 fun initialize_w_pol [] ax_weights = ax_weights
-  | initialize_w_pol ((cls,thm)::clss_thms) ax_weights =
-    let val tm = prop_of thm
-	val consts = pconsts_of_term tm
+  | initialize_w_pol ((tm,name)::tms_names) ax_weights =
+    let val consts = pconsts_of_term tm
     in
-	initialize_w_pol clss_thms (((cls,thm),(consts,0.0))::ax_weights)
+	initialize_w_pol tms_names (((tm,name),(consts,0.0))::ax_weights)
     end;
 
 
@@ -286,32 +284,31 @@
 
 
 fun relevant_clauses_ax_g_3 _ [] _ (ax,r) = (ax,r)
-  | relevant_clauses_ax_g_3 gctyps ((cls_typ,(clsthm,(consts_typs,_)))::y) P (ax,r) =
+  | relevant_clauses_ax_g_3 gctyps ((cls_typ,(clstm,(consts_typs,_)))::y) P (ax,r) =
     let val weight = find_clause_weight_s_3 gctyps consts_typs 1.0
     in
-	if P <= weight then relevant_clauses_ax_g_3 gctyps y P ((cls_typ,(clsthm,(consts_typs,weight)))::ax,r)
-	else relevant_clauses_ax_g_3 gctyps y P (ax,(cls_typ,(clsthm,(consts_typs,weight)))::r)
+	if P <= weight then relevant_clauses_ax_g_3 gctyps y P ((cls_typ,(clstm,(consts_typs,weight)))::ax,r)
+	else relevant_clauses_ax_g_3 gctyps y P (ax,(cls_typ,(clstm,(consts_typs,weight)))::r)
     end;
 
 fun relevant_clauses_ax_3 rel_axs [] P (addc,tmpc) keep =
     (case addc of [] => (rel_axs @ keep,tmpc)
 		| _ => case tmpc of [] => (addc @ rel_axs @ keep,[])
 				  | _ => relevant_clauses_ax_3 addc tmpc P ([],[]) (rel_axs @ keep))
-  | relevant_clauses_ax_3 rel_axs ((cls_typ,(clsthm,(consts_typs,weight)))::e_axs) P (addc,tmpc) keep =
+  | relevant_clauses_ax_3 rel_axs ((cls_typ,(clstm,(consts_typs,weight)))::e_axs) P (addc,tmpc) keep =
     let val weight' = find_clause_weight_m_3 rel_axs (consts_typs,weight)
-	val e_ax' = (cls_typ,(clsthm,(consts_typs,weight')))
+	val e_ax' = (cls_typ,(clstm,(consts_typs,weight')))
     in
 	if P <= weight' then relevant_clauses_ax_3 rel_axs e_axs P (e_ax'::addc,tmpc) keep
 	else relevant_clauses_ax_3 rel_axs e_axs P (addc,e_ax'::tmpc) keep
     end;
 
 fun initialize3 thy [] ax_weights = ax_weights
-  | initialize3 thy ((cls,thm)::clss_thms) ax_weights =
-    let val tm = prop_of thm
-	val cls_type = clause_type tm
+  | initialize3 thy ((tm,name)::tms_names) ax_weights =
+    let val cls_type = clause_type tm
 	val consts = consts_typs_of_term thy tm
     in
-	initialize3 thy clss_thms ((cls_type,((cls,thm),(consts,0.0)))::ax_weights)
+	initialize3 thy tms_names ((cls_type,((tm,name),(consts,0.0)))::ax_weights)
     end;
 
 fun add_unit_clauses ax [] = ax