# HG changeset patch
# User wenzelm
# Date 1288295553 -7200
# Node ID b9d15110b97ae55ea8ad7d2fdafad6c258d595d3
# Parent  7ed03c0ae420ce8b3631dff80787c8fdf882d103
eliminated dead code;

diff -r 7ed03c0ae420 -r b9d15110b97a src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Thu Oct 28 21:51:34 2010 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Thu Oct 28 21:52:33 2010 +0200
@@ -274,22 +274,6 @@
   | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
 
 (* ------------------------------------------------------------------------- *)
-(* take_prefix:                                                              *)
-(*      take_prefix n [x_1, ..., x_k] = ([x_1, ..., x_n], [x_n+1, ..., x_k]) *)
-(* ------------------------------------------------------------------------- *)
-
-(* int -> 'a list -> 'a list * 'a list *)
-
-fun take_prefix n xs =
-let
-	fun take 0 (rxs, xs)      = (rev rxs, xs)
-	  | take _ (rxs, [])      = (rev rxs, [])
-	  | take n (rxs, x :: xs) = take (n-1) (x :: rxs, xs)
-in
-	take n ([], xs)
-end;
-
-(* ------------------------------------------------------------------------- *)
 (* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
 (*      a proof from the resulting proof trace of the SAT solver.  The       *)
 (*      theorem returned is just "False" (with some of the given clauses as  *)