src/Pure/Thy/thm_deps.ML
changeset 13530 4813fdc0ef17
parent 12239 ee360f910ec8
child 14981 e73f8140af78
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Tue Aug 27 11:06:07 2002 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Tue Aug 27 11:06:20 2002 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4    let
     1.5      val _ = writeln "Generating graph ...";
     1.6      val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
     1.7 -      map (#2 o #der o Thm.rep_thm) thms))));
     1.8 +      map Thm.proof_of thms))));
     1.9      val path = File.tmp_path (Path.unpack "theorems.graph");
    1.10      val _ = Present.write_graph gra path;
    1.11      val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");