Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
the_list (cf. Pure/library.ML);
authorwenzelm
Tue, 13 Sep 2005 22:19:21 +0200
changeset 17337 5e3dde342840
parent 17336 c05f72cff368
child 17338 6b8a7bb820bb
the_list (cf. Pure/library.ML);
src/HOL/Tools/record_package.ML file | annotate | diff | comparison | revisions 
--- 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,_,_,_) =>
isabelle