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

     2.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 25 14:21:18 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 25 14:28:10 2013 +0200
     2.3 @@ -134,6 +134,8 @@
     2.4    val list_all_free: term list -> term -> term
     2.5    val list_exists_free: term list -> term -> term
     2.6  
     2.7 +  val conjuncts: term -> term list
     2.8 +
     2.9    (*parameterized terms*)
    2.10    val mk_nthN: int -> term -> int -> term
    2.11  
    2.12 @@ -637,15 +639,19 @@
    2.13  
    2.14  fun rapp u t = betapply (t, u);
    2.15  
    2.16 -val list_all_free =
    2.17 +fun list_quant_free quant_const =
    2.18    fold_rev (fn free => fn P =>
    2.19      let val (x, T) = Term.dest_Free free;
    2.20 -    in HOLogic.all_const T $ Term.absfree (x, T) P end);
    2.21 +    in quant_const T $ Term.absfree (x, T) P end);
    2.22  
    2.23 -val list_exists_free =
    2.24 -  fold_rev (fn free => fn P =>
    2.25 -    let val (x, T) = Term.dest_Free free;
    2.26 -    in HOLogic.exists_const T $ Term.absfree (x, T) P end);
    2.27 +val list_all_free = list_quant_free HOLogic.all_const;
    2.28 +val list_exists_free = list_quant_free HOLogic.exists_const;
    2.29 +
    2.30 +(*Like dest_conj, but flattens conjunctions however nested*)
    2.31 +fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
    2.32 + | conjuncts_aux t conjs = t::conjs;
    2.33 +
    2.34 +fun conjuncts t = conjuncts_aux t [];
    2.35  
    2.36  fun find_indices eq xs ys = map_filter I
    2.37    (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys);