# HG changeset patch
# User wenzelm
# Date 1121362102 -7200
# Node ID 3d5aad11bc247f38e2541fe8095444ca8aa3c3f9
# Parent  d7b47195ac7bf6af0bd0fc1b4aa99079ef76ead3
replaced Utils.itlist by fold_rev;

diff -r d7b47195ac7b -r 3d5aad11bc24 src/HOL/Tools/ATP/recon_parse.ML
--- a/src/HOL/Tools/ATP/recon_parse.ML	Thu Jul 14 19:28:21 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML	Thu Jul 14 19:28:22 2005 +0200
@@ -161,7 +161,7 @@
 
 
 fun several p = many (some p)
-      fun collect (h, t) = h ^ (Utils.itlist (fn s1 => fn s2 => s1 ^ s2) t "")
+      fun collect (h, t) = h ^ (fold_rev (fn s1 => fn s2 => s1 ^ s2) t "")
   
       fun lower_letter s = ("a" <= s) andalso (s <= "z")
       fun upper_letter s = ("A" <= s) andalso (s <= "Z")