src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
changeset 57303 498a62e65f5f
parent 56945 3d1ead21a055
child 57397 5004aca20821
--- 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