src/Pure/Isar/local_defs.ML

     val names = map2 Thm.def_binding_optional bvars bfacts;
     val eqs = mk_def ctxt (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;
   in
     ctxt
-    |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
+    |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
     |> fold Variable.declare_term eqs
     |> ProofContext.add_assms_i def_export
       (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
     |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
   end;

 fun fixed_abbrev ((x, mx), rhs) ctxt =
   let
     val T = Term.fastype_of rhs;
     val ([x'], ctxt') = ctxt
       |> Variable.declare_term rhs
-      |> ProofContext.add_fixes_i [(x, SOME T, mx)];
+      |> ProofContext.add_fixes [(x, SOME T, mx)];
     val lhs = Free (x', T);
     val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
     fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
     val (_, ctxt'') = Assumption.add_assms abbrev_export [] ctxt';
   in ((lhs, rhs), ctxt'') end;