src/HOL/Tools/old_primrec.ML
changeset 32727 9072201cd69d
parent 32712 ec5976f4d3d8
child 32863 5e8cef567042
equal deleted inserted replaced
32723:866cebde3fca 32727:9072201cd69d
   228         | SOME dt =>
   228         | SOME dt =>
   229             if tnames' subset (map (#1 o snd) (#descr dt)) then
   229             if tnames' subset (map (#1 o snd) (#descr dt)) then
   230               (tname, dt)::(find_dts dt_info tnames' tnames)
   230               (tname, dt)::(find_dts dt_info tnames' tnames)
   231             else find_dts dt_info tnames' tnames);
   231             else find_dts dt_info tnames' tnames);
   232 
   232 
   233 fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns =
   233 fun prepare_induct ({descr, induct, ...}: info) rec_eqns =
   234   let
   234   let
   235     fun constrs_of (_, (_, _, cs)) =
   235     fun constrs_of (_, (_, _, cs)) =
   236       map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
   236       map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
   237     val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
   237     val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
   238   in
   238   in