1.1 --- a/src/Pure/library.ML	Tue Jun 19 23:15:51 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Jun 19 23:15:54 2007 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Basic library: functions, options, pairs, booleans, lists, integers,
     1.7 -strings, lists as sets, balanced trees, orders, current directory, misc.
     1.8 +strings, lists as sets, orders, current directory, misc.
     1.9  
    1.10  See also General/basics.ML for the most fundamental concepts.
    1.11  *)
    1.12 @@ -194,12 +194,6 @@
    1.13    val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
    1.14    val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.15  
    1.16 -  (*balanced trees*)
    1.17 -  exception Balance
    1.18 -  val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a
    1.19 -  val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a
    1.20 -  val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list
    1.21 -
    1.22    (*orders*)
    1.23    val is_equal: order -> bool
    1.24    val rev_order: order -> order
    1.25 @@ -920,39 +914,6 @@
    1.26  
    1.27  
    1.28  
    1.29 -(** balanced trees **)
    1.30 -
    1.31 -exception Balance;      (*indicates non-positive argument to balancing fun*)
    1.32 -
    1.33 -(*balanced folding; avoids deep nesting*)
    1.34 -fun fold_bal f [x] = x
    1.35 -  | fold_bal f [] = raise Balance
    1.36 -  | fold_bal f xs =
    1.37 -      let val (ps, qs) = chop (length xs div 2) xs
    1.38 -      in  f (fold_bal f ps, fold_bal f qs)  end;
    1.39 -
    1.40 -(*construct something of the form f(...g(...(x)...)) for balanced access*)
    1.41 -fun access_bal (f, g, x) n i =
    1.42 -  let fun acc n i =     (*1<=i<=n*)
    1.43 -          if n=1 then x else
    1.44 -          let val n2 = n div 2
    1.45 -          in  if i<=n2 then f (acc n2 i)
    1.46 -                       else g (acc (n-n2) (i-n2))
    1.47 -          end
    1.48 -  in  if 1<=i andalso i<=n then acc n i else raise Balance  end;
    1.49 -
    1.50 -(*construct ALL such accesses; could try harder to share recursive calls!*)
    1.51 -fun accesses_bal (f, g, x) n =
    1.52 -  let fun acc n =
    1.53 -          if n=1 then [x] else
    1.54 -          let val n2 = n div 2
    1.55 -              val acc2 = acc n2
    1.56 -          in  if n-n2=n2 then map f acc2 @ map g acc2
    1.57 -                         else map f acc2 @ map g (acc (n-n2)) end
    1.58 -  in  if 1<=n then acc n else raise Balance  end;
    1.59 -
    1.60 -
    1.61 -
    1.62  (** orders **)
    1.63  
    1.64  fun is_equal EQUAL = true