diff -r 78fb2af1a5c3 -r 98a290c4b0b4 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Tue Apr 03 12:12:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Tue Apr 03 16:20:34 2007 +0200
@@ -723,24 +723,12 @@
   then have "e\<^isub>2[x\<^isub>2::=e'] \<Down> t\<^isub>2" using h by (simp add: trm.inject)
   thus "e'' = t\<^isub>2" using ih2 by simp
 next
-  case b_Const
-  then show ?case by force
-next
-  case b_Pr
-  then show ?case by blast
-next
   case b_Fst
   then show ?case by (force simp add: trm.inject)
 next
   case b_Snd
   then show ?case by (force simp add: trm.inject)
-next
-  case b_InL 
-  then show ?case by blast 
-next
-  case b_InR 
-  then show ?case by blast
-qed 
+qed (blast)+
 
 lemma not_val_App[simp]:
   shows