# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266597453 -3600
# Node ID fd8231b16203c8a4c4de547eb1dcbf4cd1855150
# Parent  7c7cfe69d7f6c8f7ba887de45e3d70d4b6042fd4
quote the constant and theorem name with @{text}

diff -r 7c7cfe69d7f6 -r fd8231b16203 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Feb 19 17:03:53 2010 +0100
+++ b/src/HOL/Quotient.thy	Fri Feb 19 17:37:33 2010 +0100
@@ -270,7 +270,7 @@
   In the following theorem R1 can be instantiated with anything,
   but we know some of the types of the Rep and Abs functions;
   so by solving Quotient assumptions we can get a unique R1 that
-  will be provable; which is why we need to use apply_rsp and
+  will be provable; which is why we need to use @{text apply_rsp} and
   not the primed version *}
 
 lemma apply_rsp:
@@ -465,7 +465,7 @@
   using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
   by metis
 
-section {* Bex1_rel quantifier *}
+section {* @{text Bex1_rel} quantifier *}
 
 definition
   Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"