# HG changeset patch
# User blanchet
# Date 1380120226 -7200
# Node ID ee91bd2a506a74629c2f9fdc3cd919198258f126
# Parent  c83727c7a510d655fedc2a8deba559e2cb6033c4
filled in gap in library offering

diff -r c83727c7a510 -r ee91bd2a506a src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:29:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:43:46 2013 +0200
@@ -230,7 +230,7 @@
       (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 (conds @ conjuncts cond) then_branch
+        fld (conds @ HOLogic.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
@@ -239,7 +239,7 @@
             (case dest_case ctxt s Ts t of
               NONE => f conds t
             | SOME (conds', branches) =>
-              fold_rev (uncurry fld) (map (append conds o conjuncts) conds' ~~ branches))
+              fold_rev (uncurry fld) (map (append conds o HOLogic.conjuncts) conds' ~~ branches))
           | _ => f conds t)
         end
       | _ => f conds t)
diff -r c83727c7a510 -r ee91bd2a506a src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 25 16:29:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 25 16:43:46 2013 +0200
@@ -134,8 +134,6 @@
   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
 
@@ -647,12 +645,6 @@
 val list_all_free = list_quant_free HOLogic.all_const;
 val list_exists_free = list_quant_free HOLogic.exists_const;
 
-(*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);
 
diff -r c83727c7a510 -r ee91bd2a506a src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 25 16:29:35 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 25 16:43:46 2013 +0200
@@ -43,7 +43,6 @@
   val dest_indprem : indprem -> term
   val map_indprem : (term -> term) -> indprem -> indprem
   (* general syntactic functions *)
-  val conjuncts : term -> term list
   val is_equationlike : thm -> bool
   val is_pred_equation : thm -> bool
   val is_intro : string -> thm -> bool
@@ -456,12 +455,6 @@
 
 (* general syntactic functions *)
 
-(*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 is_equationlike_term (Const ("==", _) $ _ $ _) = true
   | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
   | is_equationlike_term _ = false
diff -r c83727c7a510 -r ee91bd2a506a src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Wed Sep 25 16:29:35 2013 +0200
+++ b/src/HOL/Tools/hologic.ML	Wed Sep 25 16:43:46 2013 +0200
@@ -38,6 +38,7 @@
   val mk_imp: term * term -> term
   val mk_not: term -> term
   val dest_conj: term -> term list
+  val conjuncts: term -> term list
   val dest_disj: term -> term list
   val disjuncts: term -> term list
   val dest_imp: term -> term * term
@@ -244,6 +245,12 @@
 fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t'
   | dest_conj t = [t];
 
+(*Like dest_conj, but flattens conjunctions however nested*)
+fun conjuncts_aux (Const ("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 dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t'
   | dest_disj t = [t];