--- a/src/HOL/datatype.ML Fri Dec 19 10:18:58 1997 +0100
+++ b/src/HOL/datatype.ML Fri Dec 19 10:27:23 1997 +0100
@@ -94,7 +94,6 @@
struct
local
-val mysort = sort;
open ThyParse HOLogic;
exception Impossible;
exception RecError of string;
@@ -175,7 +174,7 @@
fun check_and_sort (n,its) =
if length its = n
- then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its)
+ then map snd (Library.sort (make_ord (fn ((i : int,_),(j,_)) => i<j)) its)
else raise error "Primrec definition error:\n\
\Please give an equation for every constructor";