# HG changeset patch
# User wenzelm
# Date 1420031330 -3600
# Node ID 36808125e00f38f6e793dc7010e3730900d996ac
# Parent  663794ab87e60cf39e936aeff8b8e49a56c0c995
uniform variable name for presentation graphs, to distinguish from values of type Graph.T

diff -r 663794ab87e6 -r 36808125e00f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:05:06 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:08:50 2014 +0100
@@ -275,7 +275,7 @@
     val thy = Toplevel.theory_of state;
     val thy_session = Present.session_name thy;
 
-    val gr = rev (Theory.nodes_of thy) |> map (fn node =>
+    val graph = rev (Theory.nodes_of thy) |> map (fn node =>
       let
         val name = Context.theory_name node;
         val parents = map Context.theory_name (Theory.parents_of node);
@@ -285,15 +285,15 @@
        {name = name, ID = name, parents = parents, dir = session,
         unfold = unfold, path = "", content = []}
       end);
-  in Graph_Display.display_graph gr end);
+  in Graph_Display.display_graph graph end);
 
 val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
     val thy = Toplevel.theory_of state;
-    val gr = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
+    val graph = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
      {name = Locale.extern thy name, ID = name, parents = parents,
       dir = "", unfold = true, path = "", content = [body]});
-  in Graph_Display.display_graph gr end);
+  in Graph_Display.display_graph graph end);
 
 
 (* print theorems, terms, types etc. *)
diff -r 663794ab87e6 -r 36808125e00f src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:05:06 2014 +0100
+++ b/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:08:50 2014 +0100
@@ -28,10 +28,10 @@
     fun entry (c, (i, (_, cs))) =
       (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
             dir = "", unfold = true, path = "", content = []});
-    val gr =
+    val graph =
       Graph.fold (cons o entry) classes []
       |> sort (int_ord o apply2 #1) |> map #2;
-  in Graph_Display.display_graph gr end;
+  in Graph_Display.display_graph graph end;
 
 val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
 val visualize_cmd = gen_visualize Syntax.read_sort;
diff -r 663794ab87e6 -r 36808125e00f src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:05:06 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:08:50 2014 +0100
@@ -926,10 +926,10 @@
     val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
     fun namify consts = map (Code.string_of_const thy) consts
       |> commas;
-    val prgr = map (fn (consts, constss) =>
+    val graph = map (fn (consts, constss) =>
       { name = namify consts, ID = namify consts, dir = "", unfold = true,
         path = "", parents = map namify constss, content = [] }) conn;
-  in Graph_Display.display_graph prgr end;
+  in Graph_Display.display_graph graph end;
 
 local