# HG changeset patch
# User Andreas Lochbihler
# Date 1338557749 -7200
# Node ID 3437685f69fbc0040602520dfc032e0a82858fef
# Parent  1f4d00a7f59fa39e3dbbf01ef74fd8c4e5e7dbf4# Parent  72197611f1e9e8e1e10c3478d77c7d3390cd4f5a
merged

diff -r 1f4d00a7f59f -r 3437685f69fb doc-src/IsarRef/isar-ref.tex
--- 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}
diff -r 1f4d00a7f59f -r 3437685f69fb doc-src/System/system.tex
--- 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}
diff -r 1f4d00a7f59f -r 3437685f69fb src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
--- 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 *}
diff -r 1f4d00a7f59f -r 3437685f69fb src/HOL/ex/set_comprehension_pointfree.ML
--- 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.
diff -r 1f4d00a7f59f -r 3437685f69fb src/Pure/System/isabelle_process.ML
--- 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;