src/HOL/Tools/datatype_prop.ML
changeset 21621 f9fd69d96c4e
parent 21078 101aefd61aac
child 22578 b0eb5652f210
equal deleted inserted replaced
21620:3d4bfc7f6363 21621:f9fd69d96c4e
   375         val tnames = make_tnames Ts;
   375         val tnames = make_tnames Ts;
   376         val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
   376         val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
   377         val ts = map (fn ((r, s), T) => List.nth (size_consts, dest_DtRec r) $
   377         val ts = map (fn ((r, s), T) => List.nth (size_consts, dest_DtRec r) $
   378           Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
   378           Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
   379         val t = if ts = [] then HOLogic.zero else
   379         val t = if ts = [] then HOLogic.zero else
   380           foldl1 plus (ts @ [HOLogic.mk_nat 1])
   380           foldl1 plus (ts @ [HOLogic.Suc_zero])
   381       in
   381       in
   382         HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
   382         HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
   383           list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t))
   383           list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t))
   384       end
   384       end
   385 
   385