changeset 39756 | 6c8e83d94536 |
parent 39276 | 2ad95934521f |
child 40076 | 6f012a209dac |
--- a/src/HOL/Tools/Function/mutual.ML Tue Sep 28 12:10:37 2010 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Tue Sep 28 12:34:41 2010 +0200 @@ -221,7 +221,7 @@ val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs val atup = foldr1 HOLogic.mk_prod avars in - tupled_lambda atup (list_comb (P, avars)) + HOLogic.tupled_lambda atup (list_comb (P, avars)) end val Ps = map2 mk_P parts newPs