diff --git a/pvs-makeindex.patch b/pvs-makeindex.patch
new file mode 100644
index 0000000..a0ef2e7
--- /dev/null
+++ b/pvs-makeindex.patch
@@ -0,0 +1,11 @@
+--- doc/user-guide/ug-commands.tex.orig	2011-04-15 11:45:08.000000000 -0600
++++ doc/user-guide/ug-commands.tex	2012-12-11 09:25:33.285718340 -0700
+@@ -1985,7 +1985,7 @@
+ 
+ The \cmd{x-show-current-proof} command creates a window showing the
+ cur\-rent proof tree.  Every sequent in the tree is represented by a
+-$\vdash$ symbol\index{"|-@$\vdash$}.  The proof commands used to create
++$\vdash$ symbol\index{_-@$\vdash$}.  The proof commands used to create
+ the tree will also be shown between the $\vdash$ symbols.  This tree will
+ be automatically updated after every proof command.
+ 
diff --git a/pvs-sbcl-5.0-index_vdash.patch b/pvs-sbcl-5.0-index_vdash.patch
deleted file mode 100644
index 5d696cb..0000000
--- a/pvs-sbcl-5.0-index_vdash.patch
+++ /dev/null
@@ -1,21 +0,0 @@
-Not exactly sure what the "|-@ is supposed to do, but it seems to
-confuse texlive-2012 in fedora 18+:
-
-! Extra }, or forgotten \endgroup.
-l.35   \item $\vdash$}
-
-So quick-n-dirty fix is to omit that part for now -- rex
-
-
-diff -up pvs-sbcl-5.0/doc/user-guide/ug-commands.tex.vdash pvs-sbcl-5.0/doc/user-guide/ug-commands.tex
---- pvs-sbcl-5.0/doc/user-guide/ug-commands.tex.vdash	2011-04-15 12:45:08.000000000 -0500
-+++ pvs-sbcl-5.0/doc/user-guide/ug-commands.tex	2012-12-10 08:48:10.022024812 -0600
-@@ -1985,7 +1985,7 @@ pathname of \texttt{wish}).
- 
- The \cmd{x-show-current-proof} command creates a window showing the
- cur\-rent proof tree.  Every sequent in the tree is represented by a
--$\vdash$ symbol\index{"|-@$\vdash$}.  The proof commands used to create
-+$\vdash$ symbol\index{$\vdash$}.  The proof commands used to create
- the tree will also be shown between the $\vdash$ symbols.  This tree will
- be automatically updated after every proof command.
- 
diff --git a/pvs-sbcl.spec b/pvs-sbcl.spec
index 4daed25..8fde9b1 100644
--- a/pvs-sbcl.spec
+++ b/pvs-sbcl.spec
@@ -1,10 +1,9 @@
-
 # workaround http://bugzilla.redhat.com/885762
 %{?!_texmf_main:%global _texmf_main %{_datadir}/texmf}
 
 Name:           pvs-sbcl
 Version:        5.0
-Release:        16%{?dist}
+Release:        17%{?dist}
 Summary:        Interactive theorem prover from SRI
 
 Group:          Applications/Engineering
@@ -30,8 +29,8 @@ Patch1:         pvs-hashfn.patch
 Patch2:         pvs-chmod.patch
 # This patch was sent upstream 20 Jan 2012.  It adapts to Emacs 24.
 Patch3:         pvs-emacs.patch
-# fix/workaround problems generating user-guide.pdf on f18+ -- rex
-Patch4:         pvs-sbcl-5.0-index_vdash.patch
+# Workaround http://bugzilla.redhat.com/886158
+Patch4:         pvs-makeindex.patch
 
 BuildRequires:  automake
 BuildRequires:  desktop-file-utils
@@ -41,11 +40,9 @@ BuildRequires:  sbcl
 BuildRequires:  texi2html
 BuildRequires:  texinfo-tex
 BuildRequires:  tex(latex)
-%if 0%{?fedora} > 17
 BuildRequires:  tex(boxedminipage.sty)
 BuildRequires:  tex(relsize.sty)
 BuildRequires:  tex(tocbibind.sty)
-%endif
 BuildRequires:  emacs
 BuildRequires:  xemacs
 BuildRequires:  xemacs-packages-extra
@@ -80,7 +77,7 @@ the lvm2 package.
 %patch1
 %patch2
 %patch3
-%patch4 -p1 -b .index_vdash
+%patch4
 
 # Upstream didn't give us a configure script
 autoreconf -i
@@ -106,7 +103,7 @@ popd
 
 # Run it once to force Lisp compilation of the native interfaces
 bin/relocate > /dev/null
-echo -e '(sb-ext:quit :recklessly-p t)' | ./pvs -raw
+./pvs -raw <<<'(sb-ext:exit :code 0 :abort t)'
 
 # We don't want the useless copy of the sbcl binary
 rm -f bin/linux/runtime/sbcl
@@ -184,7 +181,7 @@ update-desktop-database %{_datadir}/applications &>/dev/null ||:
 %files
 %doc *.ps.gz *.pdf LICENSE NOTICES README Examples
 %doc doc/PVSio-2.d.pdf doc/api/pvs-api.pdf
-%doc doc/language/language.pdf
+%doc doc/language/language.pdf doc/user-guide/user-guide.pdf
 %doc doc/prover/prover.pdf doc/release-notes/pvs-release-notes.pdf
 %{_bindir}/*
 %{_libdir}/pvs
@@ -192,6 +189,10 @@ update-desktop-database %{_datadir}/applications &>/dev/null ||:
 %{_texmf_main}/tex/latex/pvs
 
 %changelog
+* Tue Dec 11 2012 Jerry James <loganjerry@gmail.com> - 5.0-17
+- Alternate fix for the index problem
+- Distribute the user guide
+
 * Sat Dec 08 2012 Rex Dieter <rdieter@fedoraproject.org> 5.0-16
 - rebuild (sbcl)