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