# HG changeset patch
# User hoelzl
# Date 1283454511 -7200
# Node ID 606432dd1896b2bb0e2eebd850d0e45029e101a9
# Parent  e9467adb8b525232bd56541787373c88e2926a9f
Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)

diff -r e9467adb8b52 -r 606432dd1896 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Sep 02 20:44:33 2010 +0200
+++ b/src/HOL/Fun.thy	Thu Sep 02 21:08:31 2010 +0200
@@ -177,7 +177,7 @@
 lemma surj_id[simp]: "surj_on id A"
 by (simp add: surj_on_def)
 
-lemma bij_id[simp]: "bij_betw id A A"
+lemma bij_id[simp]: "bij id"
 by (simp add: bij_betw_def)
 
 lemma inj_onI: