adapted to new sort function;
authorwenzelm
Fri Dec 19 10:27:23 1997 +0100 (1997-12-19)
changeset 4448b587d40ad474
parent 4447 b7ee449eb345
child 4449 df30e75f670f
adapted to new sort function;
src/HOL/datatype.ML
src/HOL/ex/meson.ML
     1.1 --- a/src/HOL/datatype.ML	Fri Dec 19 10:18:58 1997 +0100
     1.2 +++ b/src/HOL/datatype.ML	Fri Dec 19 10:27:23 1997 +0100
     1.3 @@ -94,7 +94,6 @@
     1.4  struct
     1.5  local 
     1.6  
     1.7 -val mysort = sort;
     1.8  open ThyParse HOLogic;
     1.9  exception Impossible;
    1.10  exception RecError of string;
    1.11 @@ -175,7 +174,7 @@
    1.12  
    1.13  fun check_and_sort (n,its) = 
    1.14    if length its = n 
    1.15 -    then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its)
    1.16 +    then map snd (Library.sort (make_ord (fn ((i : int,_),(j,_)) => i<j)) its)
    1.17    else raise error "Primrec definition error:\n\
    1.18     \Please give an equation for every constructor";
    1.19  
     2.1 --- a/src/HOL/ex/meson.ML	Fri Dec 19 10:18:58 1997 +0100
     2.2 +++ b/src/HOL/ex/meson.ML	Fri Dec 19 10:27:23 1997 +0100
     2.3 @@ -312,7 +312,7 @@
     2.4  fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
     2.5  
     2.6  (*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*)
     2.7 -fun sort_clauses ths = sort fewerlits (filter (not o is_taut) ths);
     2.8 +fun sort_clauses ths = sort (make_ord fewerlits) (filter (not o is_taut) ths);
     2.9  
    2.10  (*Convert all suitable free variables to schematic variables*)
    2.11  fun generalize th = forall_elim_vars 0 (forall_intr_frees th);