# HG changeset patch
# User haftmann
# Date 1256201527 -7200
# Node ID 542b34b178ec4932c20a0cad16d8fc7c52772da0
# Parent  791a4655cae3a7519f93c38ca22d29db9aa0446a
dropped Datatype.distinct_simproc

diff -r 791a4655cae3 -r 542b34b178ec src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Oct 21 17:34:35 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 22 10:52:07 2009 +0200
@@ -26,7 +26,6 @@
   val info_of_constr : theory -> string * typ -> info option
   val info_of_case : theory -> string -> info option
   val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
-  val distinct_simproc : simproc
   val make_case :  Proof.context -> DatatypeCase.config -> string list -> term ->
     (term * term) list -> term * (term * (int * bool)) list
   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
@@ -159,49 +158,6 @@
 
 (** various auxiliary **)
 
-(* simplification procedure for showing distinctness of constructors *)
-
-fun stripT (i, Type ("fun", [_, T])) = stripT (i + 1, T)
-  | stripT p = p;
-
-fun stripC (i, f $ x) = stripC (i + 1, f)
-  | stripC p = p;
-
-val distinctN = "constr_distinct";
-
-fun distinct_rule thy ss tname eq_t = Goal.prove (Simplifier.the_context ss) [] [] eq_t
-  (K (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
-    atac 2, resolve_tac (#distinct (the_info thy tname)) 1, etac FalseE 1]));
-
-fun get_constr thy dtco =
-  get_info thy dtco
-  |> Option.map (fn { descr, index, ... } => (#3 o the o AList.lookup (op =) descr) index);
-
-fun distinct_proc thy ss (t as Const ("op =", _) $ t1 $ t2) =
-  (case (stripC (0, t1), stripC (0, t2)) of
-     ((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
-         (case (stripT (0, T1), stripT (0, T2)) of
-            ((i', Type (tname1, _)), (j', Type (tname2, _))) =>
-                if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
-                   (case get_constr thy tname1 of
-                      SOME constrs => let val cnames = map fst constrs
-                        in if cname1 mem cnames andalso cname2 mem cnames then
-                             SOME (distinct_rule thy ss tname1
-                               (Logic.mk_equals (t, HOLogic.false_const)))
-                           else NONE
-                        end
-                    | NONE => NONE)
-                else NONE
-          | _ => NONE)
-   | _ => NONE)
-  | distinct_proc _ _ _ = NONE;
-
-val distinct_simproc =
-  Simplifier.simproc @{theory HOL} distinctN ["s = t"] distinct_proc;
-
-val simproc_setup =
-  Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
-
 (* prepare datatype specifications *)
 
 fun read_typ thy ((Ts, sorts), str) =
@@ -271,7 +227,8 @@
     [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
     [], []);
 
-(* document antiquotation *)
+
+(** document antiquotation **)
 
 val _ = ThyOutput.antiquotation "datatype" Args.tyname
   (fn {source = src, context = ctxt, ...} => fn dtco =>
@@ -593,4 +550,3 @@
 end;
 
 end;
-