1.1 --- a/src/Tools/Code/code_thingol.ML	Thu Feb 23 15:15:59 2012 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Feb 23 15:49:40 2012 +0100
     1.3 @@ -908,7 +908,7 @@
     1.4    let
     1.5      fun project_consts consts (naming, program) =
     1.6        if permissive then (consts, (naming, program))
     1.7 -      else (consts, (naming, Graph.subgraph
     1.8 +      else (consts, (naming, Graph.restrict
     1.9          (member (op =) (Graph.all_succs program consts)) program));
    1.10      fun generate_consts thy algebra eqngr =
    1.11        fold_map (ensure_const thy algebra eqngr permissive);
    1.12 @@ -940,7 +940,7 @@
    1.13          val deps = Graph.immediate_succs program1 Term.dummy_patternN;
    1.14          val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
    1.15          val deps_all = Graph.all_succs program2 deps;
    1.16 -        val program3 = Graph.subgraph (member (op =) deps_all) program2;
    1.17 +        val program3 = Graph.restrict (member (op =) deps_all) program2;
    1.18        in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
    1.19    in
    1.20      ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
    1.21 @@ -1015,7 +1015,7 @@
    1.22    let
    1.23      val (_, eqngr) = Code_Preproc.obtain true thy consts [];
    1.24      val all_consts = Graph.all_succs eqngr consts;
    1.25 -  in Graph.subgraph (member (op =) all_consts) eqngr end;
    1.26 +  in Graph.restrict (member (op =) all_consts) eqngr end;
    1.27  
    1.28  fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy;
    1.29