--- a/src/HOL/Tools/datatype_prop.ML Tue Sep 25 10:27:43 2007 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Tue Sep 25 12:16:08 2007 +0200
@@ -24,8 +24,6 @@
(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 ->
@@ -61,7 +59,6 @@
in indexify_names (map type_name Ts) end;
-
(************************* injectivity of constructors ************************)
fun make_injs descr sorts =
@@ -351,44 +348,6 @@
(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 =