# HG changeset patch
# User webertj
# Date 1364396986 -3600
# Node ID 3cfd4fc428406382fbac099e1b8aaa0e3cf0c511
# Parent  13ab4f0a0b0e66645b4eb2e9b58d3aab48ea3c69
Fixed proofs to work with 13ab4f0a0b0e.

diff -r 13ab4f0a0b0e -r 3cfd4fc42840 Nominal/Ex/TypeSchemes2.thy
--- 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"