# HG changeset patch
# User wenzelm
# Date 882524039 -3600
# Node ID bcb28bb925c161d315a327e5ad69e8d3e00bcb9a
# Parent  b2ee34200dab4396fae0bae0e0728e496fc19f03
pasted old insertion sort (does not work with new sort function!)

diff -r b2ee34200dab -r bcb28bb925c1 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Dec 19 10:33:24 1997 +0100
+++ b/src/Provers/splitter.ML	Fri Dec 19 10:33:59 1997 +0100
@@ -179,6 +179,18 @@
    call split_posns with appropriate parameters
 *************************************************************)
 
+(* FIXME *)
+(*insertion sort; stable (does not reorder equal elements)
+  'less' is less-than test on type 'a*)
+fun sort (less: 'a*'a -> bool) =
+  let fun insert (x, []) = [x]
+        | insert (x, y::ys) =
+              if less(y, x) then y :: insert (x, ys) else x::y::ys;
+      fun sort1 [] = []
+        | sort1 (x::xs) = insert (x, sort1 xs)
+  in  sort1  end;
+
+
 fun select cmap state i =
   let val goali = nth_subgoal i state
       val Ts = rev(map #2 (Logic.strip_params goali))