# HG changeset patch
# User blanchet
# Date 1367501291 -7200
# Node ID b9a8c3b92a62e2af9164cc4af62384d4b180ab7a
# Parent  0a04c2a89ea9e26abf6f08196c7384fd9a5bdc7f
got rid of needless library function (find_minimum)

diff -r 0a04c2a89ea9 -r b9a8c3b92a62 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 15:08:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 15:28:11 2013 +0200
@@ -161,7 +161,6 @@
   val mk_sum_casesN: int -> int -> thm
   val mk_sum_casesN_balanced: int -> int -> thm
 
-  val find_minimum: ('b * 'b -> order) -> ('a -> 'b) -> 'a list -> 'a
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
   val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list ->
@@ -393,20 +392,6 @@
 
 val mk_union = HOLogic.mk_binop @{const_name sup};
 
-fun find_minimum _ _ [] = raise Empty
-  | find_minimum _ _ [x] = x
-  | find_minimum ord f xs =
-    let
-      fun find [x] = (f x, x)
-        | find (x :: xs) =
-          let
-            val y = f x;
-            val p' as (y', _) = find xs;
-          in
-            if ord (y', y) = LESS then p' else (y, x)
-          end;
-    in snd (find xs) end;
-
 (*dangerous; use with monotonic, converging functions only!*)
 fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);