src/HOL/Tools/BNF/bnf_fp_util.ML

   val ctor_map_uniqueN: string
   val ctor_recN: string
   val ctor_rec_o_mapN: string
   val ctor_rec_uniqueN: string
   val ctor_relN: string
+  val ctor_rel_inductN: string
   val ctor_set_inclN: string
   val ctor_set_set_inclN: string
   val disc_corecN: string
   val disc_corec_iffN: string
   val dtorN: string

   val dtor_mapN: string
   val dtor_map_coinductN: string
   val dtor_map_strong_coinductN: string
   val dtor_map_uniqueN: string
   val dtor_relN: string
+  val dtor_rel_coinductN: string
   val dtor_set_inclN: string
   val dtor_set_set_inclN: string
   val dtor_strong_coinductN: string
   val dtor_unfoldN: string
   val dtor_unfold_o_mapN: string

 val distinctN = "distinct"
 val rel_distinctN = relN ^ "_" ^ distinctN
 val injectN = "inject"
 val rel_injectN = relN ^ "_" ^ injectN
 val rel_coinductN = relN ^ "_" ^ coinductN
+val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN
 val rel_inductN = relN ^ "_" ^ inductN
+val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN
 val selN = "sel"
 val sel_corecN = selN ^ "_" ^ corecN
 
 fun co_prefix fp = (if fp = Greatest_FP then "co" else "");