src/Pure/Isar/proof.ML

       map_context_result (prep_binds false (map swap raw_rhss))
       #-> (fn rhss =>
         let
           val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
             ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
-        in map_context_result (Local_Defs.add_defs defs) end))
+        in map_context_result (Local_Defs.define defs) end))
     |-> (set_facts o map (#2 o #2))
   end;
 
 in
 

             "wrt. definitions " ^ commas (map (show_term o Free o #1 o #1) more_defs));
 
     val derived_def = Local_Defs.derived_def ctxt {conditional = false};
     val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss);
     val defs2 = match_defs decls defs1;
-    val (defs3, defs_ctxt) = Local_Defs.add_defs defs2 ctxt;
+    val (defs3, defs_ctxt) = Local_Defs.define defs2 ctxt;
 
     (*notes*)
     val def_thmss =
       map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, prove defs_ctxt th))
         (defs1 ~~ defs2 ~~ defs3)