--- a/doc-src/IsarRef/isar-ref.tex Fri Jun 01 15:33:31 2012 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Fri Jun 01 15:35:49 2012 +0200
@@ -81,10 +81,12 @@
\input{Thy/document/ML_Tactic.tex}
\begingroup
+ \tocentry{\bibname}
\bibliographystyle{abbrv} \small\raggedright\frenchspacing
\bibliography{../manual}
\endgroup
+\tocentry{\indexname}
\printindex
\end{document}
--- a/doc-src/System/system.tex Fri Jun 01 15:33:31 2012 +0200
+++ b/doc-src/System/system.tex Fri Jun 01 15:35:49 2012 +0200
@@ -35,10 +35,12 @@
\input{Thy/document/Misc.tex}
\begingroup
+ \tocentry{\bibname}
\bibliographystyle{abbrv} \small\raggedright\frenchspacing
\bibliography{../manual}
\endgroup
+\tocentry{\indexname}
\printindex
\end{document}
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Fri Jun 01 15:33:31 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Fri Jun 01 15:35:49 2012 +0200
@@ -7,7 +7,7 @@
theory Set_Comprehension_Pointfree_Tests
imports Main
-uses "~~/src/HOL/ex/set_comprehension_pointfree.ML"
+uses "set_comprehension_pointfree.ML"
begin
simproc_setup finite_Collect ("finite (Collect P)") = {* Set_Comprehension_Pointfree.simproc *}
--- a/src/HOL/ex/set_comprehension_pointfree.ML Fri Jun 01 15:33:31 2012 +0200
+++ b/src/HOL/ex/set_comprehension_pointfree.ML Fri Jun 01 15:35:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/set_comprehension_pointfree.ML
+(* Title: HOL/ex/set_comprehension_pointfree.ML
Author: Felix Kuperjans, Lukas Bulwahn, TU Muenchen
Simproc for rewriting set comprehensions to pointfree expressions.
--- a/src/Pure/System/isabelle_process.ML Fri Jun 01 15:33:31 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML Fri Jun 01 15:35:49 2012 +0200
@@ -57,7 +57,8 @@
NONE => error ("Undefined Isabelle process command " ^ quote name)
| SOME cmd =>
(Runtime.debugging cmd args handle exn =>
- error ("Isabelle process protocol failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn)));
+ error ("Isabelle process protocol failure: " ^ quote name ^ "\n" ^
+ ML_Compiler.exn_message exn)));
end;