src/FOLP/simp.ML
changeset 33339 d41f77196338
parent 33317 b4534348b8fd
child 33955 fff6f11b1f09
     1.1 --- a/src/FOLP/simp.ML	Thu Oct 29 23:49:55 2009 +0100
     1.2 +++ b/src/FOLP/simp.ML	Thu Oct 29 23:56:33 2009 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4  fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2);
     1.5  
     1.6  (*insert a thm in a discrimination net by its lhs*)
     1.7 -fun lhs_insert_thm (th,net) =
     1.8 +fun lhs_insert_thm th net =
     1.9      Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net
    1.10      handle  Net.INSERT => net;
    1.11  
    1.12 @@ -434,7 +434,7 @@
    1.13          val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
    1.14          val new_rws = maps mk_rew_rules thms;
    1.15          val rwrls = map mk_trans (maps mk_rew_rules thms);
    1.16 -        val anet' = List.foldr lhs_insert_thm anet rwrls
    1.17 +        val anet' = fold_rev lhs_insert_thm rwrls anet;
    1.18      in  if !tracing andalso not(null new_rws)
    1.19          then writeln (cat_lines
    1.20            ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))