diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
index 83bc9dbd..3f8a603e 100644
--- a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
@@ -53,7 +53,6 @@ text\<open>
 \<open>structure Data = Generic_Data
 (  type T = docobj_tab * docclass_tab * ...
    val empty  = (initial_docobj_tab, initial_docclass_tab, ...) 
-   val extend = I
    fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab  (d1,d2,...), 
                                          merge_docclass_tab(c1,c2,...))
 );\<close>}
diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
index 4c47e825..b26e71fc 100644
--- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
+++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
@@ -364,7 +364,7 @@ subsection*[t213::example]\<open>Mechanism 2 : Extending the Global Context \<op
 
 text\<open>A central mechanism for constructing user-defined data is by the \<^ML_functor>\<open>Generic_Data\<close>-functor.
   A plugin needing some data \<^verbatim>\<open>T\<close> and providing it with implementations for an 
-  \<^verbatim>\<open>empty\<close>, and operations  \<^verbatim>\<open>merge\<close> and \<^verbatim>\<open>extend\<close>, can construct a lense with operations
+  \<^verbatim>\<open>empty\<close>, and operation \<^verbatim>\<open>merge\<close>, can construct a lense with operations
   \<^verbatim>\<open>get\<close> and \<^verbatim>\<open>put\<close> that attach this data into the generic system context. Rather than using
   unsynchronized SML mutable variables, this is the mechanism to introduce component local
   data in Isabelle, which allows to manage this data for the necessary backtrack and synchronization
@@ -373,14 +373,12 @@ text\<open>A central mechanism for constructing user-defined data is by the \<^M
 ML \<open>
      datatype X = mt
      val init = mt;
-     val ext = I
      fun merge (X,Y) = mt
      
      structure Data = Generic_Data
      (
        type T = X
        val empty  = init
-       val extend = ext
        val merge  = merge
      );  
 \<close>
diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index 786d03c6..87a8e4c5 100644
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -251,7 +251,6 @@ structure Data = Generic_Data
                 docclass_eager_inv_tab = initial_docclass_eager_inv_tab,
                 docclass_lazy_inv_tab = initial_docclass_lazy_inv_tab
                } 
-  val extend =  I
   fun merge(   {docobj_tab=d1,docclass_tab = c1,
                  ISA_transformer_tab = e1, monitor_tab=m1,
                  docclass_inv_tab = n1,