--- a/ProgTutorial/General.thy	Wed Nov 11 05:34:46 2009 +0100
+++ b/ProgTutorial/General.thy	Wed Nov 11 12:15:48 2009 +0100
@@ -1358,11 +1358,11 @@
   To see how it works let us assume we defined our own theorem list @{text MyThmList}.
 *}
 
-ML{*structure MyThmList = GenericDataFun
+ML{*structure MyThmList = Generic_Data
   (type T = thm list
    val empty = []
    val extend = I
-   val merge = K (op @))
+   val merge = op @)
 
 fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*}