diff -r a789c5732f7a -r 3c544d64c218 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Wed Jun 22 14:52:27 2022 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Jun 23 19:29:22 2022 +0200
@@ -467,7 +467,7 @@
 
 lemma finite_enumerate:
   assumes fS: "finite S"
-  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono_on r {..<card S} \<and> (\<forall>n<card S. r n \<in> S)"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono_on {..<card S} r \<and> (\<forall>n<card S. r n \<in> S)"
   unfolding strict_mono_def
   using finite_enumerate_in_set[OF fS] finite_enumerate_mono[of _ _ S] fS
   by (metis lessThan_iff strict_mono_on_def)
@@ -603,11 +603,11 @@
 lemma ex_bij_betw_strict_mono_card:
   fixes M :: "'a::wellorder set"
   assumes "finite M" 
-  obtains h where "bij_betw h {..<card M} M" and "strict_mono_on h {..<card M}"
+  obtains h where "bij_betw h {..<card M} M" and "strict_mono_on {..<card M} h"
 proof
   show "bij_betw (enumerate M) {..<card M} M"
     by (simp add: assms finite_bij_enumerate)
-  show "strict_mono_on (enumerate M) {..<card M}"
+  show "strict_mono_on {..<card M} (enumerate M)"
     by (simp add: assms finite_enumerate_mono strict_mono_on_def)
 qed