1.1 --- a/src/HOL/Fun.thy	Fri Nov 26 20:52:21 2010 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Nov 26 21:09:36 2010 +0100
     1.3 @@ -155,11 +155,6 @@
     1.4    shows "inj f"
     1.5    using assms unfolding inj_on_def by auto
     1.6  
     1.7 -text{*For Proofs in @{text "Tools/Datatype/datatype_rep_proofs"}*}
     1.8 -lemma datatype_injI:
     1.9 -    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
    1.10 -by (simp add: inj_on_def)
    1.11 -
    1.12  theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
    1.13    by (unfold inj_on_def, blast)
    1.14  

     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 26 20:52:21 2010 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 26 21:09:36 2010 +0100
     2.3 @@ -19,7 +19,7 @@
     2.4  lemma injective_scaleR: 
     2.5  assumes "(c :: real) ~= 0"
     2.6  shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
     2.7 -by (metis assms datatype_injI injI real_vector.scale_cancel_left)
     2.8 +  by (metis assms injI real_vector.scale_cancel_left)
     2.9  
    2.10  lemma linear_add_cmul:
    2.11  fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" 

     3.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Nov 26 20:52:21 2010 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Nov 26 21:09:36 2010 +0100
     3.3 @@ -54,6 +54,8 @@
     3.4  val Suml_inject = @{thm Suml_inject};
     3.5  val Sumr_inject = @{thm Sumr_inject};
     3.6  
     3.7 +val datatype_injI =
     3.8 +  @{lemma "(!!x. ALL y. f x = f y --> x = y) ==> inj f" by (simp add: inj_on_def)};
     3.9  
    3.10  
    3.11  (** proof of characteristic theorems **)
    3.12 @@ -438,8 +440,7 @@
    3.13                               Lim_inject :: inj_thms') @ fun_congs) 1),
    3.14                           atac 1]))])])])]);
    3.15  
    3.16 -        val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
    3.17 -                             (split_conj_thm inj_thm);
    3.18 +        val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
    3.19  
    3.20          val elem_thm = 
    3.21              Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))