src/FOLP/ex/Nat.thy

--- a/src/FOLP/ex/Nat.thy	Sun Jul 05 15:43:45 2015 +0200
+++ b/src/FOLP/ex/Nat.thy	Sun Jul 05 16:39:25 2015 +0200
@@ -82,7 +82,9 @@
 lemmas nat_congs = Suc_cong Plus_cong
 
 ML {*
-  val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
+  val add_ss =
+    FOLP_ss addcongs @{thms nat_congs}
+    |> fold (addrew @{context}) @{thms add_0 add_Suc}
 *}
 
 schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)"