src/Pure/Thy/thy_read.ML
changeset 1514 3e262b1c0b6c
parent 1483 617ca7312ceb
child 1529 09d9ad015269
--- a/src/Pure/Thy/thy_read.ML	Mon Feb 19 09:54:52 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML	Mon Feb 19 13:54:15 1996 +0100
@@ -639,13 +639,12 @@
     (*Invoke every put method stored in the methods table to initialize
       the state of user defined variables*)
     fun init_data methods data =
-      let fun put_data [] = ()
-            | put_data ((id, date) :: ds) =
-                case Symtab.lookup (methods, id) of
-                    Some (ThyMethods {put, ...}) => put date
-                  | None => error ("No method defined for theory data \"" ^
-                                   id ^ "\"");
-      in put_data data end;
+      let fun put_data (id, date) =
+            case Symtab.lookup (methods, id) of
+                Some (ThyMethods {put, ...}) => put date
+              | None => error ("No method defined for theory data \"" ^
+                               id ^ "\"");
+      in seq put_data data end;
 
     (*Add theory to file listing all loaded theories (for index.html)
       and to the sub-charts of its parents*)