--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Mon Sep 17 16:57:22 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Mon Sep 17 21:13:30 2012 +0200
@@ -499,7 +499,9 @@
val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
fun mk_map live Ts Us t =
- let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
+ let
+ val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last
+ in
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;