fixed bug in init_data (put was only invoked for the first date)
authorclasohm
Mon, 19 Feb 1996 13:54:15 +0100
changeset 1514 3e262b1c0b6c
parent 1513 c318e1bbecca
child 1515 4ed79ebab64d
fixed bug in init_data (put was only invoked for the first date)
src/Pure/Thy/thy_read.ML
--- 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*)