src/HOL/Tools/inductive_package.ML

     val cs = map (Free o fst) cnames_syn';
     val ps = map Free pnames;
 
     val ctxt2 = lthy
       |> Variable.add_fixes (map (fst o fst) cnames_syn') |> snd
-      |> fold (snd oo LocalDefs.add_def) abbrevs;
-    val expand = Assumption.export_term ctxt2 lthy;
+      |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
+    val expand = Assumption.export_term ctxt2 lthy #> ProofContext.cert_term lthy;
 
     fun close_rule r = list_all_free (rev (fold_aterms
       (fn t as Free (v as (s, _)) =>
           if Variable.is_fixed ctxt1 s orelse
             member (op =) ps t then I else insert (op =) v

     ||> 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
-      (cnames_syn @ pnames_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs);
+    val ((vars, specs), _) = lthy |> ProofContext.set_mode ProofContext.mode_abbrev
+      |> Specification.read_specification
+          (cnames_syn @ pnames_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs);
     val (cs, ps) = chop (length cnames_syn) vars;
     val intrs = map (apsnd the_single) specs;
     val monos = Attrib.eval_thms lthy raw_monos;
     val flags = {verbose = verbose, kind = Thm.theoremK, alt_name = "",
       coind = coind, no_elim = false, no_ind = false};