# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308233510 -32400
# Node ID 39ae45d3a11baa506425e42564908bba4eca4c04
# Parent  9f667f6da04f3013975d833a94c2b82a67df3c86
Fix

diff -r 9f667f6da04f -r 39ae45d3a11b Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Thu Jun 16 22:00:52 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Jun 16 23:11:50 2011 +0900
@@ -197,6 +197,7 @@
 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")
+apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', Ta))")
 prefer 2
 apply (simp add: eqvt_at_def subst_def)
 apply rule
@@ -215,12 +216,12 @@
 apply (rule_tac x="lookup \<theta> X" in exI)
 apply clarify
 apply (rule the1_equality)
-apply metis apply assumption
+apply blast apply assumption
 apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
                   (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
 apply clarify
 apply (rule the1_equality)
-apply metis apply assumption
+apply blast apply assumption
 apply clarify
 apply simp
 --"-"