diff -r 8e3705d91cfa -r 6cf5215afe8c src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Mon Oct 26 18:04:17 2015 +0100
+++ b/src/Doc/Prog_Prove/Isar.thy	Mon Oct 26 19:00:24 2015 +0100
@@ -1021,14 +1021,14 @@
 are variables. In some rare situations one needs to deal with an assumption where
 not all arguments @{text r}, @{text s}, @{text t} are variables:
 \begin{isabelle}
-\isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}
+\isacom{lemma} @{text"\"I r s t \<Longrightarrow> \<dots>\""}
 \end{isabelle}
 Applying the standard form of
 rule induction in such a situation will lead to strange and typically unprovable goals.
 We can easily reduce this situation to the standard one by introducing
 new variables @{text x}, @{text y}, @{text z} and reformulating the goal like this:
 \begin{isabelle}
-\isacom{lemma} @{text[source]"I x y z \<Longrightarrow> x = r \<Longrightarrow> y = s \<Longrightarrow> z = t \<Longrightarrow> \<dots>"}
+\isacom{lemma} @{text"\"I x y z \<Longrightarrow> x = r \<Longrightarrow> y = s \<Longrightarrow> z = t \<Longrightarrow> \<dots>\""}
 \end{isabelle}
 Standard rule induction will work fine now, provided the free variables in
 @{text r}, @{text s}, @{text t} are generalized via @{text"arbitrary"}.
@@ -1036,7 +1036,7 @@
 However, induction can do the above transformation for us, behind the curtains, so we never
 need to see the expanded version of the lemma. This is what we need to write:
 \begin{isabelle}
-\isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}\isanewline
+\isacom{lemma} @{text"\"I r s t \<Longrightarrow> \<dots>\""}\isanewline
 \isacom{proof}@{text"(induction \"r\" \"s\" \"t\" arbitrary: \<dots> rule: I.induct)"}\index{inductionrule@@{text"induction ... rule:"}}\index{arbitrary@@{text"arbitrary:"}}
 \end{isabelle}
 Like for rule inversion, cases that are impossible because of constructor clashes