src/HOL/Tools/old_primrec.ML
changeset 32712 ec5976f4d3d8
parent 31902 862ae16a799d
child 32727 9072201cd69d
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Fri Sep 25 10:20:03 2009 +0200
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Sun Sep 27 09:52:23 2009 +0200
     1.3 @@ -230,15 +230,15 @@
     1.4                (tname, dt)::(find_dts dt_info tnames' tnames)
     1.5              else find_dts dt_info tnames' tnames);
     1.6  
     1.7 -fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
     1.8 +fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns =
     1.9    let
    1.10      fun constrs_of (_, (_, _, cs)) =
    1.11        map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
    1.12 -    val params_of = these o AList.lookup (op =) (List.concat (map constrs_of rec_eqns));
    1.13 +    val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
    1.14    in
    1.15 -    induction
    1.16 -    |> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr)))
    1.17 -    |> RuleCases.save induction
    1.18 +    induct
    1.19 +    |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
    1.20 +    |> RuleCases.save induct
    1.21    end;
    1.22  
    1.23  local