src/HOLCF/Ssum0.ML

         (rtac disjI2 1),
         (rtac exI 1),
         (rtac refl 1)
         ]);
 
-qed_goal "inj_onto_Abs_Ssum" Ssum0.thy "inj_onto Abs_Ssum Ssum"
+qed_goal "inj_on_Abs_Ssum" Ssum0.thy "inj_on Abs_Ssum Ssum"
 (fn prems =>
         [
-        (rtac inj_onto_inverseI 1),
+        (rtac inj_on_inverseI 1),
         (etac Abs_Ssum_inverse 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)
 (* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr                        *)

         "Isinl(a)=Isinr(b) ==> a=UU & b=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac noteq_SinlSinr_Rep 1),
-        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
+        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
         (rtac SsumIl 1),
         (rtac SsumIr 1)
         ]);
 
 

 "Isinl(a1)=Isinl(a2)==> a1=a2"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac inject_Sinl_Rep 1),
-        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
+        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
         (rtac SsumIl 1),
         (rtac SsumIl 1)
         ]);
 
 qed_goalw "inject_Isinr" Ssum0.thy [Isinr_def]
 "Isinr(b1)=Isinr(b2) ==> b1=b2"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac inject_Sinr_Rep 1),
-        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
+        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
         (rtac SsumIr 1),
         (rtac SsumIr 1)
         ]);
 
 qed_goal "inject_Isinl_rev" Ssum0.thy