1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sat Oct 26 12:57:17 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sat Oct 26 13:00:55 2013 +0200
     1.3 @@ -210,12 +210,10 @@
     1.4  
     1.5  fun build_rec_arg lthy (funs_data : eqn_data list list) has_call (ctr_spec : rec_ctr_spec)
     1.6      (maybe_eqn_data : eqn_data option) =
     1.7 -  if is_none maybe_eqn_data then undef_const else
     1.8 +  (case maybe_eqn_data of
     1.9 +    NONE => undef_const
    1.10 +  | SOME {ctr_args, left_args, right_args, rhs_term = t, ...} =>
    1.11      let
    1.12 -      val eqn_data = the maybe_eqn_data;
    1.13 -      val t = #rhs_term eqn_data;
    1.14 -      val ctr_args = #ctr_args eqn_data;
    1.15 -
    1.16        val calls = #calls ctr_spec;
    1.17        val n_args = fold (Integer.add o (fn Mutual_Rec _ => 2 | _ => 1)) calls 0;
    1.18  
    1.19 @@ -244,13 +242,11 @@
    1.20        val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1;
    1.21        val mutual_calls = map (apfst (nth ctr_args) o apsnd (nth args o fst)) mutual_calls';
    1.22        val nested_calls = map (apfst (nth ctr_args) o apsnd (nth args o fst)) nested_calls';
    1.23 -
    1.24 -      val abstractions = args @ #left_args eqn_data @ #right_args eqn_data;
    1.25      in
    1.26        t
    1.27        |> subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls
    1.28 -      |> fold_rev lambda abstractions
    1.29 -    end;
    1.30 +      |> fold_rev lambda (args @ left_args @ right_args)
    1.31 +    end);
    1.32  
    1.33  fun build_defs lthy bs mxs (funs_data : eqn_data list list) (rec_specs : rec_spec list) has_call =
    1.34    let
    1.35 @@ -682,12 +678,10 @@
    1.36    |> K;
    1.37  
    1.38  fun build_corec_args_mutual_call lthy has_call (sel_eqns : coeqn_data_sel list) sel =
    1.39 -  let
    1.40 -    val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
    1.41 -  in
    1.42 -    if is_none maybe_sel_eqn then (I, I, I) else
    1.43 +  (case find_first (equal sel o #sel) sel_eqns of
    1.44 +    NONE => (I, I, I)
    1.45 +  | SOME {fun_args, rhs_term, ... } =>
    1.46      let
    1.47 -      val {fun_args, rhs_term, ... } = the maybe_sel_eqn;
    1.48        val bound_Ts = List.rev (map fastype_of fun_args);
    1.49        fun rewrite_stop _ t = if has_call t then @{term False} else @{term True};
    1.50        fun rewrite_end _ t = if has_call t then undef_const else t;
    1.51 @@ -697,16 +691,13 @@
    1.52          |> abs_tuple fun_args;
    1.53      in
    1.54        (massage rewrite_stop, massage rewrite_end, massage rewrite_cont)
    1.55 -    end
    1.56 -  end;
    1.57 +    end);
    1.58  
    1.59  fun build_corec_arg_nested_call lthy has_call (sel_eqns : coeqn_data_sel list) sel =
    1.60 -  let
    1.61 -    val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
    1.62 -  in
    1.63 -    if is_none maybe_sel_eqn then I else
    1.64 +  (case find_first (equal sel o #sel) sel_eqns of
    1.65 +    NONE => I
    1.66 +  | SOME {fun_args, rhs_term, ...} =>
    1.67      let
    1.68 -      val {fun_args, rhs_term, ...} = the maybe_sel_eqn;
    1.69        val bound_Ts = List.rev (map fastype_of fun_args);
    1.70        fun rewrite bound_Ts U T (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) U T b)
    1.71          | rewrite bound_Ts U T (t as _ $ _) =
    1.72 @@ -726,29 +717,27 @@
    1.73          |> abs_tuple fun_args;
    1.74      in
    1.75        massage
    1.76 -    end
    1.77 -  end;
    1.78 +    end);
    1.79  
    1.80  fun build_corec_args_sel lthy has_call (all_sel_eqns : coeqn_data_sel list)
    1.81      (ctr_spec : corec_ctr_spec) =
    1.82 -  let val sel_eqns = filter (equal (#ctr ctr_spec) o #ctr) all_sel_eqns in
    1.83 -    if null sel_eqns then I else
    1.84 -      let
    1.85 -        val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
    1.86 -
    1.87 -        val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
    1.88 -        val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list;
    1.89 -        val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list;
    1.90 -      in
    1.91 -        I
    1.92 -        #> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls'
    1.93 -        #> fold (fn (sel, (q, g, h)) =>
    1.94 -          let val (fq, fg, fh) = build_corec_args_mutual_call lthy has_call sel_eqns sel in
    1.95 -            nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls'
    1.96 -        #> fold (fn (sel, n) => nth_map n
    1.97 -          (build_corec_arg_nested_call lthy has_call sel_eqns sel)) nested_calls'
    1.98 -      end
    1.99 -  end;
   1.100 +  (case filter (equal (#ctr ctr_spec) o #ctr) all_sel_eqns of
   1.101 +    [] => I
   1.102 +  | sel_eqns =>
   1.103 +    let
   1.104 +      val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
   1.105 +      val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
   1.106 +      val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list;
   1.107 +      val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list;
   1.108 +    in
   1.109 +      I
   1.110 +      #> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls'
   1.111 +      #> fold (fn (sel, (q, g, h)) =>
   1.112 +        let val (fq, fg, fh) = build_corec_args_mutual_call lthy has_call sel_eqns sel in
   1.113 +          nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls'
   1.114 +      #> fold (fn (sel, n) => nth_map n
   1.115 +        (build_corec_arg_nested_call lthy has_call sel_eqns sel)) nested_calls'
   1.116 +    end);
   1.117  
   1.118  fun build_codefs lthy bs mxs has_call arg_Tss (corec_specs : corec_spec list)
   1.119      (disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) =