--- a/Nominal/Ex/TypeSchemes2.thy	Wed Mar 27 16:08:30 2013 +0100
+++ b/Nominal/Ex/TypeSchemes2.thy	Wed Mar 27 16:09:46 2013 +0100
@@ -53,25 +53,13 @@
   assumes a: "\<exists>y. f x = Inl y"
   shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
 using a
-apply clarify
-apply(frule_tac p="p" in permute_boolI)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst (asm) permute_fun_app_eq)
-back
-apply(simp)
-done
+by (metis Inl_eqvt Projl_Inl permute_fun_app_eq)
 
 lemma test2:
   assumes a: "\<exists>y. f x = Inl y"
   shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
 using a
-apply clarify
-apply(frule_tac p="p" in permute_boolI)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst (asm) permute_fun_app_eq)
-back
-apply(simp)
-done
+by clarsimp
 
 nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"