src/FOLP/simp.ML
changeset 33245 65232054ffd0
parent 33063 4d462963a7db
child 33317 b4534348b8fd
     1.1 --- a/src/FOLP/simp.ML	Tue Oct 27 22:55:27 2009 +0100
     1.2 +++ b/src/FOLP/simp.ML	Tue Oct 27 22:56:14 2009 +0100
     1.3 @@ -254,13 +254,13 @@
     1.4  
     1.5  val insert_thms = fold_rev insert_thm_warn;
     1.6  
     1.7 -fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
     1.8 +fun addrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) =
     1.9  let val thms = mk_simps thm
    1.10  in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
    1.11        simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net}
    1.12  end;
    1.13  
    1.14 -val op addrews = Library.foldl addrew;
    1.15 +fun ss addrews thms = fold addrew thms ss;
    1.16  
    1.17  fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
    1.18  let val congs' = thms @ congs;
    1.19 @@ -287,7 +287,7 @@
    1.20        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
    1.21  end;
    1.22  
    1.23 -fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    1.24 +fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) =
    1.25  let fun find((p as (th,ths))::ps',ps) =
    1.26            if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    1.27        | find([],simps') =
    1.28 @@ -298,7 +298,7 @@
    1.29        simps = simps', simp_net = delete_thms thms simp_net }
    1.30  end;
    1.31  
    1.32 -val op delrews = Library.foldl delrew;
    1.33 +fun ss delrews thms = fold delrew thms ss;
    1.34  
    1.35  
    1.36  fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) =