src/HOL/Tools/hologic.ML
changeset 33245 65232054ffd0
parent 32657 5f13912245ff
child 34962 807f6ce0273d
     1.1 --- a/src/HOL/Tools/hologic.ML	Tue Oct 27 22:55:27 2009 +0100
     1.2 +++ b/src/HOL/Tools/hologic.ML	Tue Oct 27 22:56:14 2009 +0100
     1.3 @@ -638,8 +638,8 @@
     1.4      val Ts = map snd vs;
     1.5      val t = Const (c, Ts ---> T);
     1.6      val tt = mk_prod (t, Abs ("u", unitT, reflect_term t));
     1.7 -    fun app (t, (fT, (v, T))) = valapp T fT $ t $ Free (v, termifyT T);
     1.8 -  in Library.foldl app (tt, mk_fTs Ts T ~~ vs) end;
     1.9 +    fun app (fT, (v, T)) t = valapp T fT $ t $ Free (v, termifyT T);
    1.10 +  in fold app (mk_fTs Ts T ~~ vs) tt end;
    1.11  
    1.12  
    1.13  (* open state monads *)