# HG changeset patch
# User blanchet
# Date 1380112090 -7200
# Node ID 87941795956c65e32c0c1e94080211cd785ee695
# Parent  eb3075935edf318eb33fd994cab0d33b624ddc8f
break more conjunctions

diff -r eb3075935edf -r 87941795956c src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- 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)
diff -r eb3075935edf -r 87941795956c src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 25 14:21:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 25 14:28:10 2013 +0200
@@ -134,6 +134,8 @@
   val list_all_free: term list -> term -> term
   val list_exists_free: term list -> term -> term
 
+  val conjuncts: term -> term list
+
   (*parameterized terms*)
   val mk_nthN: int -> term -> int -> term
 
@@ -637,15 +639,19 @@
 
 fun rapp u t = betapply (t, u);
 
-val list_all_free =
+fun list_quant_free quant_const =
   fold_rev (fn free => fn P =>
     let val (x, T) = Term.dest_Free free;
-    in HOLogic.all_const T $ Term.absfree (x, T) P end);
+    in quant_const T $ Term.absfree (x, T) P end);
+
+val list_all_free = list_quant_free HOLogic.all_const;
+val list_exists_free = list_quant_free HOLogic.exists_const;
 
-val list_exists_free =
-  fold_rev (fn free => fn P =>
-    let val (x, T) = Term.dest_Free free;
-    in HOLogic.exists_const T $ Term.absfree (x, T) P end);
+(*Like dest_conj, but flattens conjunctions however nested*)
+fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+ | conjuncts_aux t conjs = t::conjs;
+
+fun conjuncts t = conjuncts_aux t [];
 
 fun find_indices eq xs ys = map_filter I
   (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys);