# HG changeset patch
# User wenzelm
# Date 1255986143 -7200
# Node ID 1c93cfa807bce06c25da04f13ea54761fb0a3375
# Parent  f3f02f36a3e21c4557f9640b6e4651fdc215fea0
eliminated duplicate fold1 -- beware of argument order!

diff -r f3f02f36a3e2 -r 1c93cfa807bc src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Mon Oct 19 21:54:57 2009 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Mon Oct 19 23:02:23 2009 +0200
@@ -157,8 +157,6 @@
       | _ => NONE ));
 
 
-fun foldl1 f (x::xs) = foldl f x xs;
-
 local
 val meta_ext = @{thm StateFun.meta_ext};
 val ss' = (HOL_ss addsimps
@@ -182,7 +180,7 @@
                in (Const ("Fun.comp",gT --> fT --> T)$g$f,T) end
 
              fun mk_comps fs = 
-                   foldl1 (fn ((f,fT),(g,gT)) => mk_comp f fT g gT) fs;
+                   foldl1 (fn ((f,fT),(g,gT)) => mk_comp g gT f fT) fs;
 
              fun append n c cT f fT d dT comps =
                (case AList.lookup (op aconv) comps n of