src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML

 
     fun build_applied_map TU t =
       if op = TU then
         t
       else
-        (case try (build_map ctxt [] (the o AList.lookup (op =) AB_fs)) TU of
+        (case try (build_map ctxt [] [] (the o AList.lookup (op =) AB_fs)) TU of
           SOME mapx => mapx $ t
         | NONE => raise UNNATURAL ());
 
     fun unextensionalize (f $ (x as Free _), rhs) = unextensionalize (f, lambda x rhs)
       | unextensionalize tu = tu;

       {outer_buffer = outer_buffer, ctr_guards = ctr_guards, inner_buffer = inner_buffer};
 
     fun mk_friend_spec () =
       let
         fun encapsulate_nested U T free =
-          betapply (build_map ctxt [] (fn (T, _) =>
+          betapply (build_map ctxt [] [] (fn (T, _) =>
               if T = domain_type VLeaf0_T then Abs (Name.uu, T, VLeaf0 $ Bound 0)
               else Abs (Name.uu, T, Bound 0)) (T, U),
             free);
 
         val preT = YifyT (domain_type (fastype_of ctor));