# HG changeset patch
# User wenzelm
# Date 882523643 -3600
# Node ID b587d40ad47488eb2118a71e303fb2b1b745cd5a
# Parent  b7ee449eb3454876a70c3175b666cf59fb61b0e4
adapted to new sort function;

diff -r b7ee449eb345 -r b587d40ad474 src/HOL/datatype.ML
--- 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";
 
diff -r b7ee449eb345 -r b587d40ad474 src/HOL/ex/meson.ML
--- a/src/HOL/ex/meson.ML	Fri Dec 19 10:18:58 1997 +0100
+++ b/src/HOL/ex/meson.ML	Fri Dec 19 10:27:23 1997 +0100
@@ -312,7 +312,7 @@
 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
 
 (*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*)
-fun sort_clauses ths = sort fewerlits (filter (not o is_taut) ths);
+fun sort_clauses ths = sort (make_ord fewerlits) (filter (not o is_taut) ths);
 
 (*Convert all suitable free variables to schematic variables*)
 fun generalize th = forall_elim_vars 0 (forall_intr_frees th);