src/Provers/simp.ML

 val lhs_of = #2 o dest_red;
 val rhs_of = #3 o dest_red;
 
 (*** 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) =
     Net.insert_term((lhs_of (concl_of th), (false,th)), net, eq_brl)
     handle  Net.INSERT => net;

 
 (** Insertion of congruences, rewrites and case splits **)
 
 (*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);
 
 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, 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);
 
 val delete_thms = foldr delete_thm_warn;
 
 fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
                    splits,split_consts}, 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,
       splits=splits,split_consts=split_consts}
 end;
 
 fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
               splits,split_consts}, 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'))
     val (thms,simps') = find(simps,[])
 in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,