src/HOL/datatype.ML

 
 (* check function specified for all constructors and sort function terms *)
 
 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";
 
 (* translate rec equations into function arguments suitable for rec comb *)
 (* theory parameter needed for printing error messages                   *)