tuned

jvanbruegge · Sep 17, 2024 · 8b95f55 · 8b95f55
1 parent 749af65
commit 8b95f55
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/thys/Pi_Calculus/Pi_cong.thy b/thys/Pi_Calculus/Pi_cong.thy
@@ -30,7 +30,6 @@ for perms: rrename_term rrename_term and supps: FFVars FFVars
         | ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
         | ((rule exI[of _ "\<sigma> _"])+; auto))+
   subgoal premises prems for R B P Q
-    thm prems
     apply (tactic \<open>refreshability_tac @{term B} @{term "Tsupp P Q"}
       @{thm prems(3)} @{thms emp_bound singl_bound term.Un_bound term.card_of_FFVars_bounds infinite_UNIV}
       [NONE,