src/Pure/Isar/isar_cmd.ML
changeset 49561 26fc70e983c2
parent 49012 8686c36fa27d
child 49569 7b6aaf446496
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 25 14:32:41 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 25 15:40:41 2012 +0200
     1.3 @@ -403,8 +403,11 @@
     1.4          val parents = map Context.theory_name (Theory.parents_of node);
     1.5          val session = Present.session_name node;
     1.6          val unfold = (session = thy_session);
     1.7 -      in {name = name, ID = name, parents = parents, dir = session, unfold = unfold, path = ""} end);
     1.8 -  in Present.display_graph gr end);
     1.9 +      in
    1.10 +       {name = name, ID = name, parents = parents, dir = session,
    1.11 +        unfold = unfold, path = "", content = []}
    1.12 +      end);
    1.13 +  in Graph_Display.display_graph gr end);
    1.14  
    1.15  val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.16    let
    1.17 @@ -413,11 +416,11 @@
    1.18      val classes = Sorts.classes_of algebra;
    1.19      fun entry (c, (i, (_, cs))) =
    1.20        (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
    1.21 -            dir = "", unfold = true, path = ""});
    1.22 +            dir = "", unfold = true, path = "", content = []});
    1.23      val gr =
    1.24        Graph.fold (cons o entry) classes []
    1.25        |> sort (int_ord o pairself #1) |> map #2;
    1.26 -  in Present.display_graph gr end);
    1.27 +  in Graph_Display.display_graph gr end);
    1.28  
    1.29  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.30    Thm_Deps.thm_deps (Toplevel.theory_of state)