# HG changeset patch
# User berghofe
# Date 932459657 -7200
# Node ID f59d33c6e1c7951123d4031d03fb6e6f572623b6
# Parent  3535eec33c5067c6f6c98a9a3f39141889521448
Eliminated addDistinct.

diff -r 3535eec33c50 -r f59d33c6e1c7 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Jul 19 21:26:33 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jul 20 10:34:17 1999 +0200
@@ -204,8 +204,6 @@
 
 (**** simplification procedure for showing distinctness of constructors ****)
 
-(* oracle *)
-
 val distinctN = "constr_distinct";
 
 exception ConstrDistinct of term;
@@ -248,7 +246,7 @@
   | distinct_proc sg _ _ = None;
 
 val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termTVar)];
-val distinct_simproc = mk_simproc "distinct_simproc" distinct_pats distinct_proc;
+val distinct_simproc = mk_simproc distinctN distinct_pats distinct_proc;
 
 val dist_ss = HOL_ss addsimprocs [distinct_simproc];
 
@@ -298,15 +296,6 @@
 fun store_clasimp thy (cla, simp) =
   (claset_ref_of thy := cla; simpset_ref_of thy := simp);
 
-infix 4 addDistinct;
-
-fun clasimp addDistinct ([], _) = clasimp
-  | clasimp addDistinct (thms::thmss, (_, (_, _, constrs))::descr) =
-      if length constrs < !DatatypeProp.dtK then
-        clasimp addIffs thms addDistinct (thmss, descr)
-      else
-        clasimp addsimps2 thms addDistinct (thmss, descr);
-
 
 (********************* axiomatic introduction of datatypes ********************)