1.1 --- a/src/HOL/Fun.ML	Tue Jul 20 18:50:46 1999 +0200
     1.2 +++ b/src/HOL/Fun.ML	Wed Jul 21 11:34:59 1999 +0200
     1.3 @@ -174,7 +174,7 @@
     1.4  
     1.5  (*** Lemmas about injective functions and inv ***)
     1.6  
     1.7 -Goalw [o_def] "[| inj_on f A;  inj_on g (range f) |] ==> inj_on (g o f) A";
     1.8 +Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
     1.9  by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
    1.10  qed "comp_inj_on";
    1.11