src/Pure/Thy/thm_deps.ML
changeset 26138 dc578de1d3e9
parent 24562 fc3cf01e8af1
child 26185 e53165319347
equal deleted inserted replaced
26137:9b47c8a2d869 26138:dc578de1d3e9
    66           make_deps_graph prf' (gra, parents)
    66           make_deps_graph prf' (gra, parents)
    67       end);
    67       end);
    68 
    68 
    69 fun thm_deps thms =
    69 fun thm_deps thms =
    70   Present.display_graph
    70   Present.display_graph
    71     (map snd (Symtab.dest (fst
    71     (map snd (sort_wrt fst (Symtab.dest (fst
    72       (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))));
    72       (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))))));
    73 
    73 
    74 end;
    74 end;
    75 
    75 
    76 structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
    76 structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
    77 open BasicThmDeps;
    77 open BasicThmDeps;