# HG changeset patch
# User nipkow
# Date 1213272641 -7200
# Node ID e1c49eb8cee691745d7a27580a97cf5154d7d35a
# Parent  81632fd4ff610a1a5e684b1faee30c8848843aa0
Hid swap

diff -r 81632fd4ff61 -r e1c49eb8cee6 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jun 12 11:51:47 2008 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Jun 12 14:10:41 2008 +0200
@@ -535,7 +535,7 @@
   have nSuc: "n = Suc m" by fact
   have mlessn: "m<n" by (simp add: nSuc)
   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
-  let ?hm = "swap k m h"
+  let ?hm = "Fun.swap k m h"
   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
     by (simp add: inj_on_swap_iff inj_on)
   show ?thesis
@@ -545,7 +545,7 @@
     show "m<n" by (rule mlessn)
     show "A = ?hm ` {i. i < m}" 
     proof (rule insert_image_inj_on_eq)
-      show "inj_on (swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
+      show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
       show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
       show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
 	using aA hkeq nSuc klessn
diff -r 81632fd4ff61 -r e1c49eb8cee6 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Jun 12 11:51:47 2008 +0200
+++ b/src/HOL/Fun.thy	Thu Jun 12 14:10:41 2008 +0200
@@ -460,7 +460,7 @@
   thus "inj_on f A" by simp 
 next
   assume "inj_on f A"
-  with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
+  with A show "inj_on (swap a b f) A" by(iprover intro: inj_on_imp_inj_on_swap)
 qed
 
 lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
@@ -482,6 +482,7 @@
 lemma bij_swap_iff: "bij (swap a b f) = bij f"
 by (simp add: bij_def)
 
+hide const swap
 
 subsection {* Proof tool setup *}