--- 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}
--- 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}
--- 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"
--- 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)