src/HOL/datatype.ML
changeset 4545 4eadc8c2681b
parent 4448 b587d40ad474
child 4613 67a726003cf8
equal deleted inserted replaced
4544:bd3307d3e974 4545:4eadc8c2681b
   172 
   172 
   173 (* check function specified for all constructors and sort function terms *)
   173 (* check function specified for all constructors and sort function terms *)
   174 
   174 
   175 fun check_and_sort (n,its) = 
   175 fun check_and_sort (n,its) = 
   176   if length its = n 
   176   if length its = n 
   177     then map snd (Library.sort (make_ord (fn ((i : int,_),(j,_)) => i<j)) its)
   177     then map snd (Library.sort (int_ord o pairself #1) its)
   178   else raise error "Primrec definition error:\n\
   178   else raise error "Primrec definition error:\n\
   179    \Please give an equation for every constructor";
   179    \Please give an equation for every constructor";
   180 
   180 
   181 (* translate rec equations into function arguments suitable for rec comb *)
   181 (* translate rec equations into function arguments suitable for rec comb *)
   182 (* theory parameter needed for printing error messages                   *) 
   182 (* theory parameter needed for printing error messages                   *)