diff -r d5ff8b782b29 -r fee7cfa69c50 src/Doc/Tutorial/Advanced/Partial.thy
--- a/src/Doc/Tutorial/Advanced/Partial.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Advanced/Partial.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -138,7 +138,7 @@
 *}
 
 lemma "wf(step1 f) \<longrightarrow> f(find(f,x)) = find(f,x)"
-apply(induct_tac f x rule: find.induct);
+apply(induct_tac f x rule: find.induct)
 apply simp
 done
 
@@ -191,7 +191,7 @@
   \<exists>y. while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x) = (y,y) \<and>
        f y = y"
 apply(rule_tac P = "\<lambda>(x,x'). x' = f x" and
-               r = "inv_image (step1 f) fst" in while_rule);
+               r = "inv_image (step1 f) fst" in while_rule)
 apply auto
 apply(simp add: inv_image_def step1_def)
 done