src/HOL/UNITY/Rename.thy

--- a/src/HOL/UNITY/Rename.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Rename.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -140,7 +140,7 @@
 lemma bij_rename: "bij h ==> bij (rename h)"
 apply (simp (no_asm_simp) add: rename_def bij_extend)
 done
-lemmas surj_rename = bij_rename [THEN bij_is_surj, standard]
+lemmas surj_rename = bij_rename [THEN bij_is_surj]
 
 lemma inj_rename_imp_inj: "inj (rename h) ==> inj h"
 apply (unfold inj_on_def, auto)