diff -r d157195a468a -r c6714a9562ae src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Jul 11 20:47:19 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Jul 11 21:36:42 2017 +0200
@@ -143,8 +143,9 @@
   val bnf_internals: bool Config.T
   val bnf_timing: bool Config.T
   val user_policy: fact_policy -> Proof.context -> fact_policy
-  val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context ->
-    bnf * Proof.context
+  val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> local_theory ->
+    bnf * local_theory
+  val note_bnf_defs: bnf -> local_theory -> bnf * local_theory
 
   val print_bnfs: Proof.context -> unit
   val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> bool ->
@@ -983,6 +984,22 @@
     |>> (fn [] => bnf | noted => morph_bnf (substitute_noted_thm noted) bnf)
   end;
 
+fun note_bnf_defs bnf lthy =
+  let
+    fun mk_def_binding cst_of =
+      Thm.def_binding (Binding.qualified_name (dest_Const (cst_of bnf) |> fst));
+    val notes =
+      [(mk_def_binding map_of_bnf, map_def_of_bnf bnf),
+       (mk_def_binding rel_of_bnf, rel_def_of_bnf bnf),
+       (mk_def_binding pred_of_bnf, pred_def_of_bnf bnf)] @
+      @{map 2} (pair o mk_def_binding o K) (sets_of_bnf bnf) (set_defs_of_bnf bnf)
+      |> map (fn (b, thm) => ((b, []), [([thm], [])]));
+  in
+    lthy
+    |> Local_Theory.notes notes
+    |>> (fn noted => morph_bnf (substitute_noted_thm noted) bnf)
+  end;
+
 fun mk_wit_goals zs bs sets (I, wit) =
   let
     val xs = map (nth bs) I;