--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Sun Oct 20 18:22:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Sun Oct 20 19:20:08 2013 +0200
@@ -170,11 +170,10 @@
fun subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls t =
let
- fun subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
- | subst bound_Ts (t as g' $ y) =
+ fun subst bound_Ts (t as g' $ y) =
let val y_head = head_of y in
if not (member (op =) ctr_args y_head) then
- pairself (subst bound_Ts) (g', y) |> op $
+ subst bound_Ts g' $ subst bound_Ts y
else
let
val maybe_mutual_y' = AList.lookup (op =) mutual_calls y;
@@ -185,8 +184,8 @@
primrec_error_eqn "too few arguments in recursive call" t;
in
if is_some maybe_nested_y_head' then
- massage_nested_rec_call lthy has_call
- (rewrite_map_arg get_ctr_pos) bound_Ts y_head (the maybe_nested_y_head') t
+ massage_nested_rec_call lthy has_call (rewrite_map_arg get_ctr_pos) bound_Ts y_head
+ (the maybe_nested_y_head') t
else if ctr_pos >= 0 then
(case maybe_mutual_y' of
NONE => t
@@ -195,6 +194,7 @@
t
end
end
+ | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
| subst _ t = t
in
subst [] t