# HG changeset patch
# User wenzelm
# Date 1126642761 -7200
# Node ID 5e3dde34284039e7210f25938033ea0949d61154
# Parent  c05f72cff36896710f1d5a8410a00e173851251e
the_list (cf. Pure/library.ML);

diff -r c05f72cff368 -r 5e3dde342840 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Sep 13 22:19:19 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Sep 13 22:19:21 2005 +0200
@@ -82,8 +82,6 @@
 (*** utilities ***)
 
 fun but_last xs = fst (split_last xs);
-fun list NONE = []
-  | list (SOME x) = [x]
 
 (* messages *)
 
@@ -828,7 +826,7 @@
   let
     val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg;
     val extsplits =
-            Library.foldl (fn (thms,(n,_)) => list (Symtab.curried_lookup extsplit n) @ thms)
+            Library.foldl (fn (thms,(n,_)) => the_list (Symtab.curried_lookup extsplit n) @ thms)
                     ([],dest_recTs T);
     val thms = (case get_splits sg (rec_id (~1) T) of
                    SOME (all_thm,_,_,_) =>