src/Tools/code/code_funcgr.ML
changeset 24713 8b3b6d09ef40
parent 24423 ae9cd0e92423
child 24835 8c26128f8997
     1.1 --- a/src/Tools/code/code_funcgr.ML	Tue Sep 25 17:06:14 2007 +0200
     1.2 +++ b/src/Tools/code/code_funcgr.ML	Tue Sep 25 17:06:18 2007 +0200
     1.3 @@ -328,7 +328,7 @@
     1.4  end; (*local*)
     1.5  
     1.6  structure Funcgr = CodeDataFun
     1.7 -(struct
     1.8 +(
     1.9    type T = T;
    1.10    val empty = Graph.empty;
    1.11    fun merge _ _ = Graph.empty;
    1.12 @@ -336,7 +336,7 @@
    1.13      | purge _ (SOME cs) funcgr =
    1.14          Graph.del_nodes ((Graph.all_preds funcgr 
    1.15            o filter (can (Graph.get_node funcgr))) cs) funcgr;
    1.16 -end);
    1.17 +);
    1.18  
    1.19  fun make thy =
    1.20    Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);