InductTacs.case_tac with proper context and proper declaration of local variable;
authorwenzelm
Tue Jun 10 19:15:21 2008 +0200 (2008-06-10 ago)
changeset 27128d2374ba6c02e
parent 27127 cd6617d57a16
child 27129 336807f865ce
InductTacs.case_tac with proper context and proper declaration of local variable;
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 10 19:15:20 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 10 19:15:21 2008 +0200
     1.3 @@ -94,10 +94,11 @@
     1.4                val stmnt2 = HOLogic.mk_Trueprop
     1.5                    (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
     1.6  
     1.7 -              val proof2 = fn _ => EVERY [DatatypePackage.case_tac "y" 1,
     1.8 -                                          asm_simp_tac (HOL_basic_ss addsimps simp1) 1,
     1.9 -                                          rtac @{thm exI} 1,
    1.10 -                                          rtac @{thm refl} 1]
    1.11 +              val proof2 = fn {prems, context} =>
    1.12 +                InductTacs.case_tac (context |> Variable.declare_term y) ("y", NONE) 1 THEN
    1.13 +                asm_simp_tac (HOL_basic_ss addsimps simp1) 1 THEN
    1.14 +                rtac @{thm exI} 1 THEN
    1.15 +                rtac @{thm refl} 1
    1.16  
    1.17                (* third statement *)
    1.18                val (inject_thm,thy3) =