src/HOL/Tools/inductive_package.ML

 
     val intros = map (close_rule ##> expand abbrevs') pre_intros';
   in
     ctxt
     |> mk_def flags cs intros monos params cnames_syn''
-    ||> fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs''
+    ||> fold (snd oo LocalTheory.abbrev Syntax.mode_default) abbrevs''
   end;
 
 fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
   let
     val ((vars, specs), _) = lthy |> Specification.read_specification