# 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 i