Nominal/nominal_dt_alpha.ML
changeset 2375 e163fd99de44
parent 2322 24de7e548094
child 2385 fe25a3ffeb14
--- a/Nominal/nominal_dt_alpha.ML	Mon Jul 19 14:20:23 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Mon Jul 19 16:59:43 2010 +0100
@@ -65,7 +65,9 @@
     | Set => (mk_union,  bind_set)
     | Res => (mk_union,  bind_set)
 in
-  foldl1 combine_fn (map (bind_fn lthy args) bodies)
+  bodies
+  |> map (bind_fn lthy args)
+  |> foldl1 combine_fn 
 end
 
 (* produces the term for an alpha with abstraction *)