src/HOL/Tools/datatype_package.ML

   end;
 
 
 (**** simplification procedure for showing distinctness of constructors ****)
 
-(* oracle *)
-
 val distinctN = "constr_distinct";
 
 exception ConstrDistinct of term;
 
 

           | _ => None)
    | _ => None)
   | 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];
 
 val simproc_setup =
   [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),

        nchotomy = nchotomy,
        case_cong = case_cong});
 
 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 ********************)
 
 fun add_and_get_axioms label tnames ts thy =