# HG changeset patch
# User berghofe
# Date 1190197033 -7200
# Node ID 66ef82187de1dabe060ef9b59ecca3c2646ca282
# Parent  d5e4b170d13241dd905b5172211e22916bcc072a
Enclosed end_theory in text antiquotation to make LaTeX happy.

diff -r d5e4b170d132 -r 66ef82187de1 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Sep 19 11:50:07 2007 +0200
+++ b/src/HOL/Main.thy	Wed Sep 19 12:17:13 2007 +0200
@@ -14,7 +14,7 @@
 
   \medskip Late clause setup: installs \emph{all} known theorems
   into the clause cache; cf.\ theory @{text ATP_Linkup}. 
-  FIXME: delete once end_theory actions are installed!
+  FIXME: delete once @{text end_theory} actions are installed!
 *}
 
 setup ResAxioms.clause_cache_setup