--- a/src/FOLP/simp.ML Wed Jul 13 16:07:18 2005 +0200
+++ b/src/FOLP/simp.ML Wed Jul 13 16:07:21 2005 +0200
@@ -68,7 +68,7 @@
(*insert a thm in a discrimination net by its lhs*)
fun lhs_insert_thm (th,net) =
- Net.insert_term((lhs_of (concl_of th), (false,th)), net, eq_brl)
+ Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net
handle Net.INSERT => net;
(*match subgoal i against possible theorems in the 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, Drule.eq_thm_prop)
+ Net.insert_term Drule.eq_thm_prop (concl_of th, th) net
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, Drule.eq_thm_prop)
+ Net.delete_term Drule.eq_thm_prop (concl_of th, th) net
handle Net.DELETE =>
(writeln"\nNo such rewrite or congruence rule:"; print_thm th;
net);