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 @@ -53,8 +53,8 @@
     1.4  
     1.5    val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     1.6      typ list -> term -> term -> term -> term
     1.7 -  val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     1.8 -    typ list -> typ -> term -> term
     1.9 +  val massage_direct_corec_call: Proof.context -> (term -> bool) -> (term -> term) -> typ -> term ->
    1.10 +    term
    1.11    val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
    1.12      (typ -> typ -> term -> term) -> typ list -> typ -> term -> term
    1.13    val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
    1.14 @@ -126,6 +126,9 @@
    1.15    error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
    1.16  fun ill_formed_corec_call ctxt t =
    1.17    error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
    1.18 +fun ill_formed_corec_code_rhs ctxt t =
    1.19 +  error ("Ill-formed corecursive equation right-hand side: " ^
    1.20 +    quote (Syntax.string_of_term ctxt t));
    1.21  fun invalid_map ctxt t =
    1.22    error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
    1.23  fun unexpected_rec_call ctxt t =
    1.24 @@ -193,25 +196,23 @@
    1.25      massage_call
    1.26    end;
    1.27  
    1.28 -fun massage_let_and_if ctxt check_cond massage_leaf =
    1.29 +fun massage_let_and_if ctxt check_cond massage_leaf U =
    1.30    let
    1.31 -    fun massage_rec U T t =
    1.32 +    fun massage_rec t =
    1.33        (case Term.strip_comb t of
    1.34 -        (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec U T (betapply (arg2, arg1))
    1.35 +        (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec (betapply (arg2, arg1))
    1.36        | (Const (@{const_name If}, _), arg :: args) =>
    1.37 -        list_comb (If_const U $ tap check_cond arg, map (massage_rec U T) args)
    1.38 -      | _ => massage_leaf U T t)
    1.39 +        list_comb (If_const U $ tap check_cond arg, map massage_rec args)
    1.40 +      | _ => massage_leaf t)
    1.41    in
    1.42      massage_rec
    1.43    end;
    1.44  
    1.45 -fun massage_direct_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
    1.46 -  let val typof = curry fastype_of1 bound_Ts in
    1.47 -    massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt) massage_direct_call
    1.48 -      res_U (typof t) t
    1.49 -  end;
    1.50 +fun massage_direct_corec_call ctxt has_call massage_direct_call U t =
    1.51 +  massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt) massage_direct_call
    1.52 +    U t;
    1.53  
    1.54 -fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
    1.55 +fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts U t =
    1.56    let
    1.57      val typof = curry fastype_of1 bound_Ts;
    1.58      val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
    1.59 @@ -246,7 +247,7 @@
    1.60  
    1.61      fun massage_call U T =
    1.62        massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt)
    1.63 -        (fn U => fn T => fn t =>
    1.64 +        (fn t =>
    1.65              (case U of
    1.66                Type (s, Us) =>
    1.67                (case try (dest_ctr ctxt s) t of
    1.68 @@ -264,9 +265,9 @@
    1.69                      handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
    1.70                  | _ => check_and_massage_direct_call U T t))
    1.71              | _ => ill_formed_corec_call ctxt t))
    1.72 -        U T
    1.73 +        U
    1.74    in
    1.75 -    massage_call res_U (typof t) t
    1.76 +    massage_call U (typof t) t
    1.77    end;
    1.78  
    1.79  fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;