src/Pure/Thy/thm_deps.ML
changeset 9502 50ec59aff389
parent 9450 c97dba47e504
child 11530 b6e21f6cfacd
equal deleted inserted replaced
9501:9cd32060bbc8 9502:50ec59aff389
    64 
    64 
    65 fun thm_deps thms =
    65 fun thm_deps thms =
    66   let
    66   let
    67     val _ = writeln "Generating graph ...";
    67     val _ = writeln "Generating graph ...";
    68     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
    68     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
    69       map (#der o Thm.rep_thm) thms))));
    69       map (#2 o #der o Thm.rep_thm) thms))));
    70     val path = File.tmp_path (Path.unpack "theorems.graph");
    70     val path = File.tmp_path (Path.unpack "theorems.graph");
    71     val _ = Present.write_graph gra path;
    71     val _ = Present.write_graph gra path;
    72     val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
    72     val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
    73   in () end;
    73   in () end;
    74 
    74