# HG changeset patch
# User haftmann
# Date 1403982557 -7200
# Node ID 91f9e4148460427518297e6baff5dc6e61165d2b
# Parent  2cd2ccd81f9328550ab4d9ecce7ce022a5989a16
proper trading of variables;
more appropriate ML variable names

diff -r 2cd2ccd81f93 -r 91f9e4148460 src/HOL/Library/Code_Abstract_Nat.thy
--- a/src/HOL/Library/Code_Abstract_Nat.thy	Sat Jun 28 21:09:15 2014 +0200
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Sat Jun 28 21:09:17 2014 +0200
@@ -52,6 +52,8 @@
 setup {*
 let
 
+val Suc_if_eq = Thm.incr_indexes 1 @{thm Suc_if_eq};
+
 fun remove_suc ctxt thms =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -79,7 +81,7 @@
              (Drule.instantiate'
                [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
                  SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
-               @{thm Suc_if_eq})) (Thm.forall_intr cv' thm)
+               Suc_if_eq)) (Thm.forall_intr cv' thm)
       in
         case map_filter (fn thm'' =>
             SOME (thm'', singleton