1.1 --- a/src/HOL/SizeChange/Correctness.thy	Sun Oct 18 00:10:20 2009 +0200
     1.2 +++ b/src/HOL/SizeChange/Correctness.thy	Sun Oct 18 12:07:56 2009 +0200
     1.3 @@ -1146,7 +1146,7 @@
     1.4    assumes "finite S" 
     1.5    shows "set (set2list S) = S"
     1.6    unfolding set2list_def 
     1.7 -proof (rule f_inv_f)
     1.8 +proof (rule f_inv_onto_f)
     1.9    from `finite S` have "\<exists>l. set l = S"
    1.10      by (rule finite_list)
    1.11    thus "S \<in> range set"