# HG changeset patch
# User wenzelm
# Date 884350929 -3600
# Node ID 4eadc8c2681b6574114419ac3af480a05528a4cc
# Parent  bd3307d3e974ce05cc3188aa22946861d82cbc87
eliminated make_ord;

diff -r bd3307d3e974 -r 4eadc8c2681b src/HOL/datatype.ML
--- 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";