eliminated make_ord;

--- a/src/HOL/datatype.ML	Fri Jan 09 14:01:48 1998 +0100
+++ b/src/HOL/datatype.ML	Fri Jan 09 14:02:09 1998 +0100
@@ -174,7 +174,7 @@
 
 fun check_and_sort (n,its) = 
   if length its = n 
-    then map snd (Library.sort (make_ord (fn ((i : int,_),(j,_)) => i<j)) its)
+    then map snd (Library.sort (int_ord o pairself #1) its)
   else raise error "Primrec definition error:\n\
    \Please give an equation for every constructor";