src/HOL/Codatatype/Tools/bnf_fp_util.ML

   val fld_injectN: string
   val fld_unfN: string
   val hsetN: string
   val hset_recN: string
   val inductN: string
+  val injectN: string
   val isNodeN: string
   val iterN: string
   val iter_uniqueN: string
   val lsbisN: string
   val map_simpsN: string

 val corecN = coN ^ recN
 
 val fld_unfN = fldN ^ "_" ^ unfN
 val unf_fldN = unfN ^ "_" ^ fldN
 fun mk_nchotomyN s = s ^ "_nchotomy"
-fun mk_injectN s = s ^ "_inject"
+val injectN = "inject"
+fun mk_injectN s = s ^ "_" ^ injectN
 fun mk_exhaustN s = s ^ "_exhaust"
 val fld_injectN = mk_injectN fldN
 val fld_exhaustN = mk_exhaustN fldN
 val unf_injectN = mk_injectN unfN
 val unf_exhaustN = mk_exhaustN unfN