# HG changeset patch
# User wenzelm
# Date 1324123683 -3600
# Node ID 6fe61da4c4677529e0f3505095858c98d7437d82
# Parent  143d2514347f0aa3aced8ad47adb83c7a6e8e897
tuned signature;

diff -r 143d2514347f -r 6fe61da4c467 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Dec 17 12:51:30 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Dec 17 13:08:03 2011 +0100
@@ -83,7 +83,7 @@
 
 (*******************************)
 
-val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
+val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of Datatype.distinct_lemma);
 
 
 (** simplification procedure for sorting permutations **)
@@ -769,7 +769,7 @@
           (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
         val dist =
           Drule.export_without_context
-            (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
+            (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] Datatype.distinct_lemma);
         val (thy', defs', eqns') = fold (make_constr_def tname T T')
           (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
       in
diff -r 143d2514347f -r 6fe61da4c467 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Dec 17 12:51:30 2011 +0100
+++ b/src/HOL/Set.thy	Sat Dec 17 13:08:03 2011 +0100
@@ -1560,9 +1560,6 @@
 lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
   by blast
 
-lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
-  by iprover
-
 lemma ball_simps [simp, no_atp]:
   "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
   "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
@@ -1796,7 +1793,6 @@
 val bex_triv = @{thm bex_triv}
 val bspec = @{thm bspec}
 val contra_subsetD = @{thm contra_subsetD}
-val distinct_lemma = @{thm distinct_lemma}
 val equalityCE = @{thm equalityCE}
 val equalityD1 = @{thm equalityD1}
 val equalityD2 = @{thm equalityD2}
diff -r 143d2514347f -r 6fe61da4c467 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Dec 17 12:51:30 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Dec 17 13:08:03 2011 +0100
@@ -10,6 +10,7 @@
 signature DATATYPE =
 sig
   include DATATYPE_DATA
+  val distinct_lemma: thm
   type spec =
     (binding * (string * sort) list * mixfix) *
     (binding * typ list * mixfix) list
@@ -28,6 +29,7 @@
 
 (** auxiliary **)
 
+val distinct_lemma = @{lemma "f x \<noteq> f y ==> x \<noteq> y" by iprover};
 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
 
 val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
diff -r 143d2514347f -r 6fe61da4c467 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Dec 17 12:51:30 2011 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Dec 17 13:08:03 2011 +0100
@@ -20,16 +20,12 @@
 structure Rep_Datatype: REP_DATATYPE =
 struct
 
-type config = Datatype_Aux.config;
-type descr = Datatype_Aux.descr;
-
-
-
 (** derived definitions and proofs **)
 
 (* case distinction theorems *)
 
-fun prove_casedist_thms (config : config) new_type_names descr induct case_names_exhausts thy =
+fun prove_casedist_thms (config : Datatype_Aux.config)
+    new_type_names descr induct case_names_exhausts thy =
   let
     val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
 
@@ -76,7 +72,7 @@
 
 (* primrec combinators *)
 
-fun prove_primrec_thms (config : config) new_type_names descr
+fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr
     injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
   let
     val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
@@ -273,7 +269,8 @@
 
 (* case combinators *)
 
-fun prove_case_thms (config : config) new_type_names descr reccomb_names primrec_thms thy =
+fun prove_case_thms (config : Datatype_Aux.config)
+    new_type_names descr reccomb_names primrec_thms thy =
   let
     val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ...";
 
@@ -348,7 +345,7 @@
 
 (* case splitting *)
 
-fun prove_split_thms (config : config)
+fun prove_split_thms (config : Datatype_Aux.config)
     new_type_names case_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
   let
     val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
@@ -398,7 +395,7 @@
 
 (* additional theorems for TFL *)
 
-fun prove_nchotomys (config : config) new_type_names descr casedist_thms thy =
+fun prove_nchotomys (config : Datatype_Aux.config) new_type_names descr casedist_thms thy =
   let
     val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";