proper trading of variables;
authorhaftmann
Sat Jun 28 21:09:17 2014 +0200 (2014-06-28)
changeset 5742791f9e4148460
parent 57426 2cd2ccd81f93
child 57428 47c8475e7864
proper trading of variables;
more appropriate ML variable names
src/HOL/Library/Code_Abstract_Nat.thy
     1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Sat Jun 28 21:09:15 2014 +0200
     1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Sat Jun 28 21:09:17 2014 +0200
     1.3 @@ -52,6 +52,8 @@
     1.4  setup {*
     1.5  let
     1.6  
     1.7 +val Suc_if_eq = Thm.incr_indexes 1 @{thm Suc_if_eq};
     1.8 +
     1.9  fun remove_suc ctxt thms =
    1.10    let
    1.11      val thy = Proof_Context.theory_of ctxt;
    1.12 @@ -79,7 +81,7 @@
    1.13               (Drule.instantiate'
    1.14                 [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
    1.15                   SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
    1.16 -               @{thm Suc_if_eq})) (Thm.forall_intr cv' thm)
    1.17 +               Suc_if_eq)) (Thm.forall_intr cv' thm)
    1.18        in
    1.19          case map_filter (fn thm'' =>
    1.20              SOME (thm'', singleton