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);