# HG changeset patch
# User haftmann
# Date 1238254412 -3600
# Node ID b3c851b0ea39526fc6872a680b2a14fc2fc7b2e9
# Parent  78d12065c638f3696537120695c7e3839dcf6450# Parent  16c689643a7a3f0e001acbc47b2b9bb6c46cbf14
merged

diff -r 78d12065c638 -r b3c851b0ea39 doc-src/Codegen/Thy/pictures/adaption.tex
--- 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 16:33:32 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}
diff -r 78d12065c638 -r b3c851b0ea39 doc-src/Codegen/Thy/pictures/architecture.tex
--- 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 16:33:32 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}
diff -r 78d12065c638 -r b3c851b0ea39 src/Pure/Isar/code_unit.ML
--- 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 16:33:32 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"
diff -r 78d12065c638 -r b3c851b0ea39 src/Tools/code/code_target.ML
--- 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 16:33:32 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)