src/HOL/Library/Code_Abstract_Nat.thy
changeset 57427 91f9e4148460
parent 57426 2cd2ccd81f93
child 58881 b9556a055632
     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