src/HOL/Library/bnf_decl.ML

       Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
     val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
     val Fwits = map2 (fn witb => fn witT =>
       Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
     val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
-      prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads))
+      prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
       user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
       lthy;
 
     fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;