src/FOLP/simp.ML
changeset 30190 479806475f3c
parent 29265 5b4247055bd7
child 32091 30e2ffbba718
     1.1 --- a/src/FOLP/simp.ML	Sun Mar 01 16:48:06 2009 +0100
     1.2 +++ b/src/FOLP/simp.ML	Sun Mar 01 23:36:12 2009 +0100
     1.3 @@ -433,7 +433,7 @@
     1.4          val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
     1.5          val new_rws = List.concat(map mk_rew_rules thms);
     1.6          val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
     1.7 -        val anet' = foldr lhs_insert_thm anet rwrls
     1.8 +        val anet' = List.foldr lhs_insert_thm anet rwrls
     1.9      in  if !tracing andalso not(null new_rws)
    1.10          then (writeln"Adding rewrites:";  Display.prths new_rws;  ())
    1.11          else ();