changeset 16709 | a4679ac06502 |
parent 16685 | 4ffc943c9c75 |
child 16806 | 916387f7afd2 |
--- 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),