1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Sep 30 17:47:50 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Sep 30 17:53:44 2013 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4        primrec_error_eqn "recursive call not directly applied to constructor argument" t)
     1.5    end;
     1.6  
     1.7 -fun build_rec_arg lthy funs_data has_call ctr_spec maybe_eqn_data =
     1.8 +fun build_rec_arg lthy (funs_data : eqn_data list) has_call ctr_spec maybe_eqn_data =
     1.9    if is_none maybe_eqn_data then undef_const else
    1.10      let
    1.11        val eqn_data = the maybe_eqn_data;
    1.12 @@ -243,7 +243,7 @@
    1.13        |> fold_rev lambda abstractions
    1.14      end;
    1.15  
    1.16 -fun build_defs lthy bs mxs funs_data rec_specs has_call =
    1.17 +fun build_defs lthy bs mxs (funs_data : eqn_data list) rec_specs has_call =
    1.18    let
    1.19      val n_funs = length funs_data;
    1.20  
    1.21 @@ -275,7 +275,7 @@
    1.22      |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs
    1.23    end;
    1.24  
    1.25 -fun find_rec_calls has_call eqn_data =
    1.26 +fun find_rec_calls has_call (eqn_data : eqn_data) =
    1.27    let
    1.28      fun find (Abs (_, _, b)) ctr_arg = find b ctr_arg
    1.29        | find (t as _ $ _) ctr_arg =
    1.30 @@ -329,8 +329,8 @@
    1.31  
    1.32      val defs = build_defs lthy' bs mxs funs_data rec_specs has_call;
    1.33  
    1.34 -    fun prove def_thms' {ctr_specs, nested_map_idents, nested_map_comps, ...} induct_thm fun_data
    1.35 -        lthy =
    1.36 +    fun prove def_thms' ({nested_map_idents, nested_map_comps, ctr_specs, ...} : rec_spec)
    1.37 +        induct_thm fun_data lthy =
    1.38        let
    1.39          val fun_name = #fun_name (hd fun_data);
    1.40          val def_thms = map (snd o snd) def_thms';
    1.41 @@ -397,6 +397,7 @@
    1.42    auto_gen: bool,
    1.43    user_eqn: term
    1.44  };
    1.45 +
    1.46  type co_eqn_data_sel = {
    1.47    fun_name: string,
    1.48    fun_T: typ,
    1.49 @@ -406,6 +407,7 @@
    1.50    rhs_term: term,
    1.51    user_eqn: term
    1.52  };
    1.53 +
    1.54  datatype co_eqn_data =
    1.55    Disc of co_eqn_data_disc |
    1.56    Sel of co_eqn_data_sel;