src/HOL/Nominal/nominal_primrec.ML

   end;
 
 fun thy_note ((name, atts), thms) =
   PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
 fun thy_def false ((name, atts), t) =
-      PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
+      PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
   | thy_def true ((name, atts), t) =
-      PureThy.add_defs_unchecked_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+      PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
 
 in
 
 val add_primrec = gen_primrec thy_note (thy_def false);
 val add_primrec_unchecked = gen_primrec thy_note (thy_def true);