--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 14:21:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 14:28:10 2013 +0200
@@ -230,7 +230,8 @@
(case Term.strip_comb t of
(Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
| (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
- fld (cond :: conds) then_branch o fld (s_not cond :: conds) else_branch
+ fld (conds @ conjuncts cond) then_branch
+ o fld (conds @ s_not_disj cond) else_branch
| (Const (c, _), args as _ :: _) =>
let val n = num_binder_types (Sign.the_const_type thy c) in
(case fastype_of1 (bound_Ts, nth args (n - 1)) of
@@ -238,7 +239,7 @@
(case dest_case ctxt s Ts t of
NONE => f conds t
| SOME (conds', branches) =>
- fold_rev (uncurry fld) (map (fn cond => cond :: conds) conds' ~~ branches))
+ fold_rev (uncurry fld) (map (append conds o conjuncts) conds' ~~ branches))
| _ => f conds t)
end
| _ => f conds t)