--- a/src/FOLP/simp.ML Sun Mar 01 16:48:06 2009 +0100
+++ b/src/FOLP/simp.ML Sun Mar 01 23:36:12 2009 +0100
@@ -433,7 +433,7 @@
val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
val new_rws = List.concat(map mk_rew_rules thms);
val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
- val anet' = foldr lhs_insert_thm anet rwrls
+ val anet' = List.foldr lhs_insert_thm anet rwrls
in if !tracing andalso not(null new_rws)
then (writeln"Adding rewrites:"; Display.prths new_rws; ())
else ();