# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1601042092 -3600
# Node ID 6fdeef6d6335047b454dc77f27ddeb418158ce15
# Parent  4e649ea1f76be7f664c345c0791a47ab858092c8
reverted the substitution here

diff -r 4e649ea1f76b -r 6fdeef6d6335 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Fri Sep 25 14:12:01 2020 +0100
+++ b/src/HOL/Library/Permutations.thy	Fri Sep 25 14:54:52 2020 +0100
@@ -334,14 +334,14 @@
   case (insert x F)
   {
     fix n
-    assume card.insert_remove: "card (insert x F) = n"
+    assume card_insert: "card (insert x F) = n"
     let ?xF = "{p. p permutes insert x F}"
     let ?pF = "{p. p permutes F}"
     let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
     let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
     have xfgpF': "?xF = ?g ` ?pF'"
       by (rule permutes_insert[of x F])
-    from \<open>x \<notin> F\<close> \<open>finite F\<close> card.insert_remove have Fs: "card F = n - 1"
+    from \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have Fs: "card F = n - 1"
       by auto
     from \<open>finite F\<close> insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
       by auto
@@ -383,13 +383,13 @@
       then show ?thesis
         unfolding inj_on_def by blast
     qed
-    from \<open>x \<notin> F\<close> \<open>finite F\<close> card.insert_remove have "n \<noteq> 0"
+    from \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have "n \<noteq> 0"
       by auto
     then have "\<exists>m. n = Suc m"
       by presburger
     then obtain m where n: "n = Suc m"
       by blast
-    from pFs card.insert_remove have *: "card ?xF = fact n"
+    from pFs card_insert have *: "card ?xF = fact n"
       unfolding xfgpF' card_image[OF ginj]
       using \<open>finite F\<close> \<open>finite ?pF\<close>
       by (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product) (simp add: n)