diff -r 479f7ac538b5 -r a4679ac06502 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Jul 06 10:41:42 2005 +0200
+++ b/src/Pure/simplifier.ML	Wed Jul 06 10:41:43 2005 +0200
@@ -478,7 +478,7 @@
 fun simp_flags x = (Scan.repeat
   (Args.parens (Args.$$$ "depth_limit" -- Args.colon |-- Args.nat)
     >> setmp MetaSimplifier.simp_depth_limit)
-  >> curry (Library.foldl op o) I) x;
+  >> (curry (Library.foldl op o) I o rev)) x;
 
 val cong_modifiers =
  [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),