diff -r 03bee3a6a1b7 -r 3d7a695385f1 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Wed Sep 05 19:51:00 2012 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Wed Sep 05 20:19:37 2012 +0200
@@ -321,7 +321,7 @@
 proof (nominal_induct e e\<^isub>1 avoiding: e\<^isub>2 rule: big.strong_induct)
   case (b_Lam x e t\<^isub>2)
   have "Lam [x].e \<Down> t\<^isub>2" by fact
-  thus "Lam [x].e = t\<^isub>2" by (cases, simp_all add: trm.inject)
+  thus "Lam [x].e = t\<^isub>2" by cases (simp_all add: trm.inject)
 next
   case (b_App x e\<^isub>1 e\<^isub>2 e' e\<^isub>1' e\<^isub>2' t\<^isub>2)
   have ih1: "\<And>t. e\<^isub>1 \<Down> t \<Longrightarrow> Lam [x].e\<^isub>1' = t" by fact