# HG changeset patch
# User wenzelm
# Date 1290802176 -3600
# Node ID acb8302071032a04bb91351fc09470f20e2a051e
# Parent  4d72119686073c47dd173f48a4a8c068dfbc089b
keep private things private, without comments;

diff -r 4d7211968607 -r acb830207103 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Nov 26 20:52:21 2010 +0100
+++ b/src/HOL/Fun.thy	Fri Nov 26 21:09:36 2010 +0100
@@ -155,11 +155,6 @@
   shows "inj f"
   using assms unfolding inj_on_def by auto
 
-text{*For Proofs in @{text "Tools/Datatype/datatype_rep_proofs"}*}
-lemma datatype_injI:
-    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
-by (simp add: inj_on_def)
-
 theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
   by (unfold inj_on_def, blast)
 
diff -r 4d7211968607 -r acb830207103 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 26 20:52:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 26 21:09:36 2010 +0100
@@ -19,7 +19,7 @@
 lemma injective_scaleR: 
 assumes "(c :: real) ~= 0"
 shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
-by (metis assms datatype_injI injI real_vector.scale_cancel_left)
+  by (metis assms injI real_vector.scale_cancel_left)
 
 lemma linear_add_cmul:
 fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" 
diff -r 4d7211968607 -r acb830207103 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Nov 26 20:52:21 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Nov 26 21:09:36 2010 +0100
@@ -54,6 +54,8 @@
 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 **)
@@ -438,8 +440,7 @@
                              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))