src/HOL/Tools/Datatype/datatype.ML

 val Inl_inject = @{thm Inl_inject};
 val Inr_inject = @{thm Inr_inject};
 val Suml_inject = @{thm Suml_inject};
 val Sumr_inject = @{thm Sumr_inject};
 
+val datatype_injI =
+  @{lemma "(!!x. ALL y. f x = f y --> x = y) ==> inj f" by (simp add: inj_on_def)};
 
 
 (** proof of characteristic theorems **)
 
 fun representation_proofs (config : config) (dt_info : info Symtab.table)

                          REPEAT (eresolve_tac (mp :: allE ::
                            map make_elim (Suml_inject :: Sumr_inject ::
                              Lim_inject :: inj_thms') @ fun_congs) 1),
                          atac 1]))])])])]);
 
-        val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
-                             (split_conj_thm inj_thm);
+        val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
 
         val elem_thm = 
             Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
               (fn _ =>
                EVERY [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,