diff -r 1a8f08f9f8af -r 630b8dd0b31a src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Feb 15 17:09:25 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Feb 15 17:09:45 2006 +0100
@@ -45,6 +45,7 @@
   val `|--> : iexpr list * iexpr -> iexpr;
 
   type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
+  type datatyp = (vname * sort) list * (string * itype list) list;
   datatype prim =
       Pretty of Pretty.T
     | Name;
@@ -53,7 +54,7 @@
     | Prim of (string * prim list) list
     | Fun of funn
     | Typesyn of (vname * sort) list * itype
-    | Datatype of (vname * sort) list * (string * itype list) list
+    | Datatype of datatyp
     | Datatypecons of string
     | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
     | Classmember of class
@@ -72,6 +73,7 @@
   val ensure_prim: string -> string -> module -> module;
   val get_def: module -> string -> def;
   val merge_module: module * module -> module;
+  val diff_module: module * module -> (string * def) list;
   val partof: string list -> module -> module;
   val has_nsp: string -> string -> bool;
   val succeed: 'a -> transact -> 'a transact_fin;
@@ -379,6 +381,7 @@
 (* type definitions *)
 
 type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
+type datatyp = (vname * sort) list * (string * itype list) list;
 
 datatype prim =
     Pretty of Pretty.T
@@ -389,7 +392,7 @@
   | Prim of (string * prim list) list
   | Fun of funn
   | Typesyn of (vname * sort) list * itype
-  | Datatype of (vname * sort) list * (string * itype list) list
+  | Datatype of datatyp
   | Datatypecons of string
   | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
   | Classmember of class
@@ -672,6 +675,23 @@
       | join_module name _ = raise Graph.DUP name
   in Graph.join join_module modl12 end;
 
+fun diff_module modl12 =
+  let
+    fun diff_entry prefix modl2 (name, Def def1) = 
+          let
+            val e2 = try (Graph.get_node modl2) name
+          in if is_some e2 andalso eq_def (def1, (dest_def o the) e2)
+            then I
+            else cons (NameSpace.pack (prefix @ [name]), def1)
+          end
+      | diff_entry prefix modl2 (name, Module modl1) =
+          diff_modl (prefix @ [name]) (modl1,
+            (the_default empty_module o Option.map dest_modl o try (Graph.get_node modl2)) name)
+    and diff_modl prefix (modl1, modl2) =
+      fold (diff_entry prefix modl2)
+        ((AList.make (Graph.get_node modl1) o Library.flat o Graph.strong_conn) modl1)
+  in diff_modl [] modl12 [] end;
+
 fun partof names modl =
   let
     datatype pathnode = PN of (string list * (string * pathnode) list);