src/FOLP/simp.ML

 
 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) =
-    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.
   Similar to match_from_nat_tac, but the net does not contain numbers;
   rewrite rules are not ordered.*)

 
 (** Insertion of congruences and rewrites **)
 
 (*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);
 
 val insert_thms = foldr insert_thm_warn;

 
 (** Deletion of congruences and rewrites **)
 
 (*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);
 
 val delete_thms = foldr delete_thm_warn;