# HG changeset patch
# User haftmann
# Date 1242064464 -7200
# Node ID 54092b86ef8190bfe0cd9166a20eb392bae442df
# Parent  0ce5f53fc65d56cc3f747cbfb9002cb3a38c6b9c
avoid latex output problem

diff -r 0ce5f53fc65d -r 54092b86ef81 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon May 11 17:20:52 2009 +0200
+++ b/src/HOL/Predicate.thy	Mon May 11 19:54:24 2009 +0200
@@ -669,7 +669,7 @@
 code_const Seq and Empty and Insert and Join
   (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
 
-text {* dummy setup for code_pred keyword *}
+text {* dummy setup for @{text code_pred} keyword *}
 
 ML {*
 OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"