# 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