pasted old insertion sort (does not work with new sort function!)
authorwenzelm
Fri Dec 19 10:33:59 1997 +0100 (1997-12-19)
changeset 4453bcb28bb925c1
parent 4452 b2ee34200dab
child 4454 2e089fae6ed7
pasted old insertion sort (does not work with new sort function!)
src/Provers/splitter.ML
     1.1 --- a/src/Provers/splitter.ML	Fri Dec 19 10:33:24 1997 +0100
     1.2 +++ b/src/Provers/splitter.ML	Fri Dec 19 10:33:59 1997 +0100
     1.3 @@ -179,6 +179,18 @@
     1.4     call split_posns with appropriate parameters
     1.5  *************************************************************)
     1.6  
     1.7 +(* FIXME *)
     1.8 +(*insertion sort; stable (does not reorder equal elements)
     1.9 +  'less' is less-than test on type 'a*)
    1.10 +fun sort (less: 'a*'a -> bool) =
    1.11 +  let fun insert (x, []) = [x]
    1.12 +        | insert (x, y::ys) =
    1.13 +              if less(y, x) then y :: insert (x, ys) else x::y::ys;
    1.14 +      fun sort1 [] = []
    1.15 +        | sort1 (x::xs) = insert (x, sort1 xs)
    1.16 +  in  sort1  end;
    1.17 +
    1.18 +
    1.19  fun select cmap state i =
    1.20    let val goali = nth_subgoal i state
    1.21        val Ts = rev(map #2 (Logic.strip_params goali))