# HG changeset patch
# User haftmann
# Date 1249030148 -7200
# Node ID 36dbff4841ab9360972b36ca58e7abbe90bf1dc4
# Parent  36017d1ea1b3ffb00e81688296ac8a4eb326ef81
repair mess produced by resolution afterwards

diff -r 36017d1ea1b3 -r 36dbff4841ab 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;