diff -r 27f3c10b0b50 -r 4cf66f21b764 src/HOL/Isar_Examples/Structured_Statements.thy
--- a/src/HOL/Isar_Examples/Structured_Statements.thy	Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy	Mon Dec 07 10:38:04 2015 +0100
@@ -152,9 +152,9 @@
 
   have C
   proof -
-    show ?thesis when "A x" (is ?A) for x :: 'a  -- \<open>abstract @{term x}\<close>
+    show ?thesis when "A x" (is ?A) for x :: 'a  \<comment> \<open>abstract @{term x}\<close>
       using that sorry
-    show "?A a"  -- \<open>concrete @{term a}\<close>
+    show "?A a"  \<comment> \<open>concrete @{term a}\<close>
       sorry
   qed
 end