1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 01:09:25 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 01:09:25 2013 +0200
     1.3 @@ -57,8 +57,8 @@
     1.4      term
     1.5    val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
     1.6      (typ -> typ -> term -> term) -> typ list -> typ -> term -> term
     1.7 -  val massage_corec_code_rhs: Proof.context -> (term -> bool) -> (term -> term list -> term) ->
     1.8 -    typ list -> typ -> term -> term
     1.9 +  val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
    1.10 +  val massage_corec_code_rhs: Proof.context -> (term -> term list -> term) -> typ -> term -> term
    1.11    val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
    1.12      ((term * term list list) list) list -> local_theory ->
    1.13      (bool * rec_spec list * typ list * thm * thm list) * local_theory
    1.14 @@ -267,7 +267,7 @@
    1.15      massage_call U (typof t) t
    1.16    end;
    1.17  
    1.18 -fun explode_ctr_term ctxt s Ts t =
    1.19 +fun expand_ctr_term ctxt s Ts t =
    1.20    (case fp_sugar_of ctxt s of
    1.21      SOME fp_sugar =>
    1.22      let
    1.23 @@ -284,19 +284,18 @@
    1.24      in
    1.25        Const (@{const_name Let}, T --> (T --> T) --> T) $ t $ Abs (Name.uu, T, xif)
    1.26      end
    1.27 -  | NONE => raise Fail "explode_ctr_term");
    1.28 +  | NONE => raise Fail "expand_ctr_term");
    1.29  
    1.30 -fun massage_corec_code_rhs ctxt has_call massage_ctr bound_Ts U t =
    1.31 -  let val typof = curry fastype_of1 bound_Ts in
    1.32 -    (case typof t of
    1.33 -      T as Type (s, Ts) =>
    1.34 -      massage_let_and_if ctxt has_call (fn t =>
    1.35 -        (case try (dest_ctr ctxt s) t of
    1.36 -          SOME (f, args) => massage_ctr f args
    1.37 -        | NONE => massage_let_and_if ctxt has_call (uncurry massage_ctr o Term.strip_comb) T
    1.38 -            (explode_ctr_term ctxt s Ts t))) U t
    1.39 -    | _ => raise Fail "massage_corec_code_rhs")
    1.40 -  end;
    1.41 +fun expand_corec_code_rhs ctxt has_call bound_Ts t =
    1.42 +  (case fastype_of1 (bound_Ts, t) of
    1.43 +    T as Type (s, Ts) =>
    1.44 +    massage_let_and_if ctxt has_call (fn t =>
    1.45 +      if can (dest_ctr ctxt s) t then t
    1.46 +      else massage_let_and_if ctxt has_call I T (expand_ctr_term ctxt s Ts t)) T t
    1.47 +  | _ => raise Fail "expand_corec_code_rhs");
    1.48 +
    1.49 +fun massage_corec_code_rhs ctxt massage_ctr =
    1.50 +  massage_let_and_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
    1.51  
    1.52  fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
    1.53  fun indexedd xss = fold_map indexed xss;