# HG changeset patch
# User wenzelm
# Date 1147367716 -7200
# Node ID 2545e8ab59a5c7eca9a8551794722fd5d561dbbf
# Parent  e3ab6cd838a41909dfbea4f0eaac283e724ed6c8
replaced Graph.fold_nodes by general Graph.fold;

diff -r e3ab6cd838a4 -r 2545e8ab59a5 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Thu May 11 19:15:15 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Thu May 11 19:15:16 2006 +0200
@@ -616,11 +616,11 @@
 
 fun fold_defs f =
   let
-    fun fol prfix (name, Def def) =
+    fun fol prfix (name, (Def def, _)) =
           f (NameSpace.pack (prfix @ [name]), def)
-      | fol prfix (name, Module modl) =
-          Graph.fold_nodes (fol (prfix @ [name])) modl
-  in Graph.fold_nodes (fol []) end;
+      | fol prfix (name, (Module modl, _)) =
+          Graph.fold (fol (prfix @ [name])) modl
+  in Graph.fold (fol []) end;
 
 fun add_deps f modl =
   modl
@@ -742,9 +742,9 @@
   let
     (*fun submodules prfx modl =
       cons prfx
-      #> Graph.fold_nodes
-          (fn (m, Module modl) => submodules (prfx @ [m]) modl
-            | (_, Def _) => I) modl;
+      #> Graph.fold
+          (fn (m, (Module modl, _)) => submodules (prfx @ [m]) modl
+            | (_, (Def _, _)) => I) modl;
     fun get_modl name =
       fold (fn n => fn modl => (dest_modl oo Graph.get_node) modl n) name modl*)
     fun imports prfx [] modl =