diff -r 58f02fbaa764 -r 498a62e65f5f src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Jun 24 13:48:14 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Jun 24 13:48:14 2014 +0200
@@ -239,7 +239,7 @@
   let
     fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
 
-    val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd);
+    val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd);
 
     fun massage_mutual_call bound_Ts U T t =
       if has_call t then