Fix POPLmark after rebase

jvanbruegge · Sep 19, 2024 · 2d82511 · 2d82511
1 parent 424d010
commit 2d82511
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/thys/POPLmark/POPLmark_1A.thy b/thys/POPLmark/POPLmark_1A.thy
@@ -108,6 +108,7 @@ using assms(1,2) proof (binder_induction \<Gamma> "\<forall>X<:S\<^sub>1. S\<^su
       apply (rule ty.equiv)
        apply (rule bij_swap supp_swap_bound infinite_var)+
         apply (rule SA_All(6))
+        apply (unfold map_context_def[symmetric])
      apply (subst extend_eqvt)
        apply (rule bij_swap supp_swap_bound infinite_var)+
      apply (rule arg_cong3[of _ _ _ _ _ _ extend])
@@ -144,6 +145,7 @@ using assms(1,2) proof (binder_induction \<Gamma> S "\<forall>X<:T\<^sub>1. T\<^
       apply (rule ty.equiv)
        apply (rule bij_swap supp_swap_bound infinite_var)+
         apply (rule SA_All(6))
+        apply (unfold map_context_def[symmetric])
      apply (subst extend_eqvt)
        apply (rule bij_swap supp_swap_bound infinite_var)+
      apply (rule arg_cong3[of _ _ _ _ _ _ extend])

diff --git a/thys/POPLmark/SystemFSub.thy b/thys/POPLmark/SystemFSub.thy
@@ -328,8 +328,8 @@ binder_inductive ty
         apply (erule cong[OF cong[OF cong], THEN iffD1, of R, OF refl, rotated -1]) back
           apply (drule ty_fresh_extend)
           apply (simp_all add: supp_swap_bound)
-        apply (rule context_map_cong_id; auto)
-        done
+          by (metis image_eqI map_context_def map_context_swap_FFVars)
+      done
     done
   done