diff -r 64ed05609568 -r 8b3b6d09ef40 src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Tue Sep 25 17:06:14 2007 +0200
+++ b/src/Tools/code/code_funcgr.ML	Tue Sep 25 17:06:18 2007 +0200
@@ -328,7 +328,7 @@
 end; (*local*)
 
 structure Funcgr = CodeDataFun
-(struct
+(
   type T = T;
   val empty = Graph.empty;
   fun merge _ _ = Graph.empty;
@@ -336,7 +336,7 @@
     | purge _ (SOME cs) funcgr =
         Graph.del_nodes ((Graph.all_preds funcgr 
           o filter (can (Graph.get_node funcgr))) cs) funcgr;
-end);
+);
 
 fun make thy =
   Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);