src/HOL/Tools/BNF/bnf_axiomatization.ML

     fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
     val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
 
     val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
-      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
+      (Specification.axiomatization [] [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
 
     fun mk_wit_thms set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
         (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
       |> Thm.close_derivation