1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Jul 31 09:46:09 2009 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jul 31 10:49:08 2009 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4      val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
     1.5    in
     1.6      if forall (can dest) thms andalso exists (contains_suc o dest) thms
     1.7 -      then perhaps_loop (remove_suc thy) thms
     1.8 +      then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
     1.9         else NONE
    1.10    end;
    1.11