# HG changeset patch
# User wenzelm
# Date 1236214538 -3600
# Node ID 2fab27ea2a1fba1814f0c56d641a53abb12b1094
# Parent  5af6ed62385b60dc4eabe73aa405457975d5a33b
updated generated file -- changed since @{ML} now ignores source flag;

diff -r 5af6ed62385b -r 2fab27ea2a1f doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Thu Mar 05 00:16:28 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Thu Mar 05 01:55:38 2009 +0100
@@ -503,7 +503,7 @@
   \item \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}} defines a named simplification
   procedure that is invoked by the Simplifier whenever any of the
   given term patterns match the current redex.  The implementation,
-  which is provided as ML source text, needs to be of type \verb|"morphism -> simpset -> cterm -> thm option"|, where the \verb|cterm| represents the current redex \isa{r} and the result is
+  which is provided as ML source text, needs to be of type \verb|morphism -> simpset -> cterm -> thm option|, where the \verb|cterm| represents the current redex \isa{r} and the result is
   supposed to be some proven rewrite rule \isa{{\isachardoublequote}r\ {\isasymequiv}\ r{\isacharprime}{\isachardoublequote}} (or a
   generalized version), or \verb|NONE| to indicate failure.  The
   \verb|simpset| argument holds the full context of the current