src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML

           Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT);
         val spec =
           mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
           |> Syntax.check_term lthy;
         val ((_, (_, raw_def)), lthy') =
-          Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
+          Specification.definition NONE [] (Attrib.empty_binding, spec) lthy;
         val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
         val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
       in
         (def, lthy')
       end;