--- a/src/HOL/Bali/Table.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Bali/Table.thy Thu Sep 26 10:51:29 2002 +0200
@@ -213,7 +213,7 @@
done
lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
-apply (rule injI)
+apply (rule inj_onI)
apply auto
done