src/HOL/Library/Efficient_Nat.thy

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