src/FOL/ex/Classical.thy

--- a/src/FOL/ex/Classical.thy	Mon Oct 19 23:00:07 2015 +0200
+++ b/src/FOL/ex/Classical.thy	Mon Oct 19 23:07:17 2015 +0200
@@ -322,8 +322,8 @@
 
 text \<open>
   Other proofs: Can use @{text auto}, which cheats by using rewriting!
-  Deepen_tac alone requires 253 secs.  Or
-  by (mini_tac 1 THEN Deepen_tac 5 1)
+  @{text Deepen_tac} alone requires 253 secs.  Or
+  @{text \<open>by (mini_tac 1 THEN Deepen_tac 5 1)\<close>}.
 \<close>
 
 text\<open>44\<close>