--- a/src/FOLP/simp.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/FOLP/simp.ML Tue May 07 14:26:32 2002 +0200
@@ -64,7 +64,7 @@
(*** Indexing and filtering of theorems ***)
-fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2);
+fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop (th1,th2);
(*insert a thm in a discrimination net by its lhs*)
fun lhs_insert_thm (th,net) =
@@ -247,7 +247,7 @@
(*insert a thm in a thm net*)
fun insert_thm_warn (th,net) =
- Net.insert_term((concl_of th, th), net, eq_thm)
+ Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
handle Net.INSERT =>
(writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
net);
@@ -273,7 +273,7 @@
(*delete a thm from a thm net*)
fun delete_thm_warn (th,net) =
- Net.delete_term((concl_of th, th), net, eq_thm)
+ Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
handle Net.DELETE =>
(writeln"\nNo such rewrite or congruence rule:"; print_thm th;
net);
@@ -281,7 +281,7 @@
val delete_thms = foldr delete_thm_warn;
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
-let val congs' = foldl (gen_rem eq_thm) (congs,thms)
+let val congs' = foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
in SS{auto_tac=auto_tac, congs= congs',
cong_net= delete_thms(map mk_trans thms,cong_net),
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
@@ -289,7 +289,7 @@
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
let fun find((p as (th,ths))::ps',ps) =
- if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
+ if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
| find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
print_thm thm;
([],simps'))