src/FOLP/simp.ML
changeset 16800 90eff1b52428
parent 15574 b1d1b5bfc464
child 16876 f57b38cced32
     1.1 --- a/src/FOLP/simp.ML	Wed Jul 13 16:07:18 2005 +0200
     1.2 +++ b/src/FOLP/simp.ML	Wed Jul 13 16:07:21 2005 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  
     1.5  (*insert a thm in a discrimination net by its lhs*)
     1.6  fun lhs_insert_thm (th,net) =
     1.7 -    Net.insert_term((lhs_of (concl_of th), (false,th)), net, eq_brl)
     1.8 +    Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net
     1.9      handle  Net.INSERT => net;
    1.10  
    1.11  (*match subgoal i against possible theorems in the net.
    1.12 @@ -247,7 +247,7 @@
    1.13  
    1.14  (*insert a thm in a thm net*)
    1.15  fun insert_thm_warn (th,net) = 
    1.16 -  Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
    1.17 +  Net.insert_term Drule.eq_thm_prop (concl_of th, th) net
    1.18    handle Net.INSERT => 
    1.19      (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
    1.20       net);
    1.21 @@ -273,7 +273,7 @@
    1.22  
    1.23  (*delete a thm from a thm net*)
    1.24  fun delete_thm_warn (th,net) = 
    1.25 -  Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
    1.26 +  Net.delete_term Drule.eq_thm_prop (concl_of th, th) net
    1.27    handle Net.DELETE => 
    1.28      (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
    1.29       net);