diff -r 259073d16f84 -r 188e2924433e src/HOL/Isar_examples/MultisetOrder.thy
--- a/src/HOL/Isar_examples/MultisetOrder.thy	Tue Feb 22 21:49:34 2000 +0100
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Tue Feb 22 21:50:02 2000 +0100
@@ -22,8 +22,8 @@
     (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
   (concl is "?case1 (mult1 r) | ?case2");
 proof (unfold mult1_def);
-  let ?r = "\<lambda>K a. ALL b. elem K b --> (b, a) : r";
-  let ?R = "\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
+  let ?r = "\\<lambda>K a. ALL b. elem K b --> (b, a) : r";
+  let ?R = "\\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
   let ?case1 = "?case1 {(N, M). ?R N M}";
 
   assume "(N, M0 + {#a#}) : {(N, M). ?R N M}";
@@ -84,7 +84,7 @@
 	assume N: "N = M0 + K";
 	assume "ALL b. elem K b --> (b, a) : r";
 	have "?this --> M0 + K : ?W" (is "?P K");
-	proof (induct K rule: multiset_induct);
+	proof (induct K in rule: multiset_induct);
 	  from M0; have "M0 + {#} : ?W"; by simp;
 	  thus "?P {#}"; ..;
 
@@ -109,7 +109,7 @@
   assume wf: "wf r";
   fix M;
   show "M : ?W";
-  proof (induct M rule: multiset_induct);
+  proof (induct M in rule: multiset_induct);
     show "{#} : ?W";
     proof (rule accI);
       fix b; assume "(b, {#}) : ?R";