src/FOLP/simp.ML
changeset 22360 26ead7ed4f4b
parent 21287 a713ae348e8a
child 22578 b0eb5652f210
     1.1 --- a/src/FOLP/simp.ML	Mon Feb 26 21:34:16 2007 +0100
     1.2 +++ b/src/FOLP/simp.ML	Mon Feb 26 23:18:24 2007 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  
     1.5  (*** Indexing and filtering of theorems ***)
     1.6  
     1.7 -fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Drule.eq_thm_prop (th1, th2);
     1.8 +fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2);
     1.9  
    1.10  (*insert a thm in a discrimination net by its lhs*)
    1.11  fun lhs_insert_thm (th,net) =
    1.12 @@ -248,7 +248,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 Drule.eq_thm_prop (concl_of th, th) net
    1.17 +  Net.insert_term Thm.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 @@ -274,7 +274,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 Drule.eq_thm_prop (concl_of th, th) net
    1.26 +  Net.delete_term Thm.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);
    1.30 @@ -282,7 +282,7 @@
    1.31  val delete_thms = fold_rev delete_thm_warn;
    1.32  
    1.33  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
    1.34 -let val congs' = fold (remove Drule.eq_thm_prop) thms congs
    1.35 +let val congs' = fold (remove Thm.eq_thm_prop) thms congs
    1.36  in SS{auto_tac=auto_tac, congs= congs',
    1.37        cong_net= delete_thms (map mk_trans thms) cong_net,
    1.38        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
    1.39 @@ -290,7 +290,7 @@
    1.40  
    1.41  fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    1.42  let fun find((p as (th,ths))::ps',ps) =
    1.43 -          if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    1.44 +          if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    1.45        | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
    1.46                             print_thm thm;
    1.47                             ([],simps'))