--- a/ProgTutorial/FirstSteps.thy	Wed Nov 11 05:34:46 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Wed Nov 11 12:15:48 2009 +0100
@@ -1054,22 +1054,21 @@
   maintained inside a proof context, which represents ``local'' data.
 
   For theories and proof contexts there are, respectively, the functors 
-  @{ML_funct_ind TheoryDataFun} and @{ML_funct_ind ProofDataFun} that help
+  @{ML_funct_ind Theory_Data} and @{ML_funct_ind Proof_Data} that help
   with the data storage. Below we show how to implement a table in which you
   can store theorems and look them up according to a string key. The
   intention in this example is to be able to look up introduction rules for logical
   connectives. Such a table might be useful in an automatic proof procedure
   and therefore it makes sense to store this data inside a theory.  
-  Consequently we use the functor @{ML_funct TheoryDataFun}.
+  Consequently we use the functor @{ML_funct Theory_Data}.
   The code for the table is:
 *}
 
-ML %linenosgray{*structure Data = TheoryDataFun
+ML %linenosgray{*structure Data = Theory_Data
   (type T = thm Symtab.table
    val empty = Symtab.empty
-   val copy = I
    val extend = I
-   fun merge _ = Symtab.merge (K true))*}
+   val merge = Symtab.merge (K true))*}
 
 text {*
   In order to store data in a theory, we have to specify the type of the data
@@ -1077,14 +1076,14 @@
   which stands for a table in which @{ML_type string}s can be looked up
   producing an associated @{ML_type thm}. We also have to specify four
   functions to use this functor: namely how to initialise the data storage
-  (Line 3), how to copy it (Line 4), how to extend it (Line 5) and how two
-  tables should be merged (Line 6). These functions correspond roughly to the
+  (Line 3), how to extend it (Line 4) and how two
+  tables should be merged (Line 5). These functions correspond roughly to the
   operations performed on theories and we just give some sensible 
   defaults.\footnote{\bf FIXME: Say more about the
   assumptions of these operations.} The result structure @{ML_text Data}
   contains functions for accessing the table (@{ML Data.get}) and for updating
-  it (@{ML Data.map}). There are also two more functions (@{ML Data.init} and
-  @{ML Data.put}), which however are not relevant here. Below we define two
+  it (@{ML Data.map}). There is also the functions @{ML Data.put}, which however is 
+  not relevant here. Below we define two
   auxiliary functions, which help us with accessing the table.
 *}
 
@@ -1133,12 +1132,11 @@
   integers.
 *}
 
-ML{*structure WrongRefData = TheoryDataFun
+ML{*structure WrongRefData = Theory_Data
   (type T = (int list) Unsynchronized.ref
    val empty = Unsynchronized.ref []
-   val copy = I
    val extend = I
-   fun merge _ = fst)*}
+   val merge = fst)*}
 
 text {*
   We initialise the reference with the empty list. Consequently a first 
@@ -1196,11 +1194,11 @@
   \end{readmore}
 
   Storing data in a proof context is done in a similar fashion. As mentioned
-  before, the corresponding functor is @{ML_funct_ind ProofDataFun}. With the
+  before, the corresponding functor is @{ML_funct_ind Proof_Data}. With the
   following code we can store a list of terms in a proof context.
 *}
 
-ML{*structure Data = ProofDataFun
+ML{*structure Data = Proof_Data
   (type T = term list
    fun init _ = [])*}