1.1 --- a/src/HOL/UNITY/Extend.thy	Sun Oct 18 00:10:20 2009 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.thy	Sun Oct 18 12:07:56 2009 +0200
     1.3 @@ -121,12 +121,7 @@
     1.4       assumes surj_h: "surj h"
     1.5           and prem:   "!! x y. g (h(x,y)) = x"
     1.6       shows "fst (inv h z) = g z"
     1.7 -apply (unfold inv_def)
     1.8 -apply (rule_tac y1 = z in surj_h [THEN surjD, THEN exE])
     1.9 -apply (rule someI2)
    1.10 -apply (drule_tac [2] f = g in arg_cong)
    1.11 -apply (auto simp add: prem)
    1.12 -done
    1.13 +by (metis UNIV_I f_inv_onto_f pair_collapse prem surj_h surj_range)
    1.14  
    1.15  
    1.16  subsection{*Trivial properties of f, g, h*}