# HG changeset patch
# User nipkow
# Date 932549699 -7200
# Node ID 9b6bdced3dc632b1370791cc0b924b1333e36d09
# Parent  c70d3402fef57e1d71877b02d42ad1209a26b7e0
Mod by Norber Voelcker

diff -r c70d3402fef5 -r 9b6bdced3dc6 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Tue Jul 20 18:50:46 1999 +0200
+++ b/src/HOL/Fun.ML	Wed Jul 21 11:34:59 1999 +0200
@@ -174,7 +174,7 @@
 
 (*** Lemmas about injective functions and inv ***)
 
-Goalw [o_def] "[| inj_on f A;  inj_on g (range f) |] ==> inj_on (g o f) A";
+Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
 by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
 qed "comp_inj_on";