src/HOL/SPARK/Tools/spark_vcs.ML

         val _ = T = T' orelse
           error ("Declared type " ^ ty ^ " of " ^ s ^
             "\ndoes not match type " ^ ty' ^ " in definition");
         val id' = mk_rulename id;
         val ((t', (_, th)), lthy') = Named_Target.theory_init thy
-          |> Specification.definition NONE []
+          |> Specification.definition NONE [] []
             ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
         val phi =
           Proof_Context.export_morphism lthy'
             (Proof_Context.init_global (Proof_Context.theory_of lthy'));
       in