src/HOL/Tools/datatype_prop.ML

     (string * sort) list -> theory -> term list list
   val make_distincts : string list -> DatatypeAux.descr list ->
     (string * sort) list -> theory -> term list list
   val make_splits : string list -> DatatypeAux.descr list ->
     (string * sort) list -> theory -> (term * term) list
-  val make_size : DatatypeAux.descr list -> (string * sort) list ->
-    theory -> term list
   val make_weak_case_congs : string list -> DatatypeAux.descr list ->
     (string * sort) list -> theory -> term list
   val make_case_congs : string list -> DatatypeAux.descr list ->
     (string * sort) list -> theory -> term list
   val make_nchotomys : DatatypeAux.descr list ->

     fun type_name (TFree (name, _)) = implode (tl (explode name))
       | type_name (Type (name, _)) = 
           let val name' = Sign.base_name name
           in if Syntax.is_identifier name' then name' else "x" end;
   in indexify_names (map type_name Ts) end;
-
 
 
 (************************* injectivity of constructors ************************)
 
 fun make_injs descr sorts =

 
   in map make_split ((hd descr) ~~ newTs ~~
     (make_case_combs new_type_names descr sorts thy "f"))
   end;
 
-
-(******************************* size functions *******************************)
-
-fun make_size descr sorts thy =
-  let
-    val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
-
-    val Const (size_name, _) = HOLogic.size_const dummyT;
-    val size_names = replicate (length (hd descr)) size_name @
-      map (Sign.intern_const thy) (indexify_names
-        (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
-    val size_consts = map (fn (s, T) =>
-      Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
-
-    fun plus (t1, t2) = Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
-
-    fun make_size_eqn size_const T (cname, cargs) =
-      let
-        val recs = filter is_rec_type cargs;
-        val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val recTs = map (typ_of_dtyp descr' sorts) recs;
-        val tnames = make_tnames Ts;
-        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
-        val ts = map (fn ((r, s), T) => nth size_consts (dest_DtRec r) $
-          Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
-        val t = if ts = [] then HOLogic.zero else
-          foldl1 plus (ts @ [HOLogic.Suc_zero])
-      in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
-          list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t))
-      end
-
-  in
-    List.concat (map (fn (((_, (_, _, constrs)), size_const), T) =>
-      map (make_size_eqn size_const T) constrs) (descr' ~~ size_consts ~~ recTs))
-  end;
-
 (************************* additional rules for TFL ***************************)
 
 fun make_weak_case_congs new_type_names descr sorts thy =
   let
     val case_combs = make_case_combs new_type_names descr sorts thy "f";