src/Tools/Code/code_namespace.ML
changeset 45218 700008399ee5
parent 44208 47cf4bc789aa
child 48447 b32aae03e3d6
     1.1 --- a/src/Tools/Code/code_namespace.ML	Sat Aug 20 22:46:19 2011 +0200
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Sat Aug 20 23:35:30 2011 +0200
     1.3 @@ -86,7 +86,8 @@
     1.4        end;
     1.5      val proto_program = Graph.empty
     1.6        |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
     1.7 -      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
     1.8 +      |> Graph.fold (fn (name, (_, (_, names))) =>
     1.9 +          Graph.Keys.fold (add_dependency name) names) program;
    1.10  
    1.11      (* name declarations and statement modifications *)
    1.12      fun declare name (base, stmt) (gr, nsp) = 
    1.13 @@ -191,7 +192,8 @@
    1.14        in (map_module name_fragments_common o apsnd) add_edge end;
    1.15      val proto_program = empty_program
    1.16        |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
    1.17 -      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
    1.18 +      |> Graph.fold (fn (name, (_, (_, names))) =>
    1.19 +          Graph.Keys.fold (add_dependency name) names) program;
    1.20  
    1.21      (* name declarations, data and statement modifications *)
    1.22      fun make_declarations nsps (data, nodes) =