--- 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;