# HG changeset patch
# User schirmer
# Date 1083662708 -7200
# Node ID 64844b4cc10777769ffaa5e11397fb389f3c152c
# Parent  62a724ce51c7b818257c9d6c902b9f407b8c72df
solved sml-nj compatibility problem

diff -r 62a724ce51c7 -r 64844b4cc107 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue May 04 11:24:02 2004 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue May 04 11:25:08 2004 +0200
@@ -1227,8 +1227,8 @@
     foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) (parent_exts,extT);
 
 (* record_definition *)
-
-fun record_definition (args, bname) parent parents raw_fields thy = 
+fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy = 
+  (* smlnj needs type annotation of parents *)
   let
     val sign = Theory.sign_of thy;