merged

--- a/doc-src/Codegen/Thy/pictures/adaption.tex	Sat Mar 28 12:26:21 2009 +0100
+++ b/doc-src/Codegen/Thy/pictures/adaption.tex	Sat Mar 28 18:17:44 2009 +0100
@@ -6,6 +6,12 @@
 
 \begin{document}
 
+\thispagestyle{empty}
+\setlength{\fboxrule}{0.01pt}
+\setlength{\fboxsep}{4pt}
+
+\fbox{
+
 \begin{tikzpicture}[scale = 0.5]
   \tikzstyle water=[color = blue, thick]
   \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
@@ -43,4 +49,6 @@
     (adaption) -- (reserved);
 \end{tikzpicture}
 
+}
+
 \end{document}

--- a/doc-src/Codegen/Thy/pictures/architecture.tex	Sat Mar 28 12:26:21 2009 +0100
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex	Sat Mar 28 18:17:44 2009 +0100
@@ -6,6 +6,12 @@
 
 \begin{document}
 
+\thispagestyle{empty}
+\setlength{\fboxrule}{0.01pt}
+\setlength{\fboxsep}{4pt}
+
+\fbox{
+
 \begin{tikzpicture}[x = 4.2cm, y = 1cm]
   \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
   \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
@@ -30,4 +36,6 @@
   \draw [style=process_arrow] (seri) -- (Haskell);
 \end{tikzpicture}
 
+}
+
 \end{document}

--- a/src/Pure/Isar/code_unit.ML	Sat Mar 28 12:26:21 2009 +0100
+++ b/src/Pure/Isar/code_unit.ML	Sat Mar 28 18:17:44 2009 +0100
@@ -325,19 +325,18 @@
     val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
       handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
           | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
-    fun vars_of t = fold_aterms
-     (fn Var (v, _) => insert (op =) v
-       | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
-           ^ Display.string_of_thm thm)
-       | _ => I) t [];
-    fun tvars_of t = fold_term_types
-     (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v
-                          | TFree _ => bad_thm 
+    fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
+      | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
+          ^ Display.string_of_thm thm)
+      | _ => I) t [];
+    fun tvars_of t = fold_term_types (fn _ =>
+      fold_atyps (fn TVar (v, _) => insert (op =) v
+        | TFree _ => bad_thm 
       ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t [];
     val lhs_vs = vars_of lhs;
     val rhs_vs = vars_of rhs;
     val lhs_tvs = tvars_of lhs;
-    val rhs_tvs = tvars_of lhs;
+    val rhs_tvs = tvars_of rhs;
     val _ = if null (subtract (op =) lhs_vs rhs_vs)
       then ()
       else bad_thm ("Free variables on right hand side of rewrite theorem\n"

--- a/src/Tools/code/code_target.ML	Sat Mar 28 12:26:21 2009 +0100
+++ b/src/Tools/code/code_target.ML	Sat Mar 28 18:17:44 2009 +0100
@@ -411,7 +411,7 @@
     val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
     val names2 = subtract (op =) names_hidden names1;
     val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
-    val names_all = Graph.all_succs program2 names2;
+    val names_all = Graph.all_succs program3 names2;
     val includes = abs_includes names_all;
     val program4 = Graph.subgraph (member (op =) names_all) program3;
     val empty_funs = filter_out (member (op =) abortable)

--- a/src/Tools/code/code_wellsorted.ML	Sat Mar 28 12:26:21 2009 +0100
+++ b/src/Tools/code/code_wellsorted.ML	Sat Mar 28 18:17:44 2009 +0100
@@ -353,14 +353,20 @@
 fun code_deps thy consts =
   let
     val eqngr = code_depgr thy consts;
-    fun mk_entry (const, (_, (_, parents))) =
-      let
-        val name = Code_Unit.string_of_const thy const;
-        val nameparents = map (Code_Unit.string_of_const thy) parents;
-      in { name = name, ID = name, dir = "", unfold = true,
-        path = "", parents = nameparents }
-      end;
-    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) eqngr [];
+    val constss = Graph.strong_conn eqngr;
+    val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
+      Symtab.update (const, consts)) consts) constss;
+    fun succs consts = consts
+      |> maps (Graph.imm_succs eqngr)
+      |> subtract (op =) consts
+      |> map (the o Symtab.lookup mapping)
+      |> distinct (op =);
+    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
+    fun namify consts = map (Code_Unit.string_of_const thy) consts
+      |> commas;
+    val prgr = map (fn (consts, constss) =>
+      { name = namify consts, ID = namify consts, dir = "", unfold = true,
+        path = "", parents = map namify constss }) conn;
   in Present.display_graph prgr end;
 
 local