# HG changeset patch
# User wenzelm
# Date 1213118121 -7200
# Node ID d2374ba6c02e1575b7aec24cbcda0ef328622e48
# Parent  cd6617d57a1660307cff2c4d26a14c7b5fb9d0b3
InductTacs.case_tac with proper context and proper declaration of local variable;

diff -r cd6617d57a16 -r d2374ba6c02e src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 10 19:15:20 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 10 19:15:21 2008 +0200
@@ -94,10 +94,11 @@
               val stmnt2 = HOLogic.mk_Trueprop
                   (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
 
-              val proof2 = fn _ => EVERY [DatatypePackage.case_tac "y" 1,
-                                          asm_simp_tac (HOL_basic_ss addsimps simp1) 1,
-                                          rtac @{thm exI} 1,
-                                          rtac @{thm refl} 1]
+              val proof2 = fn {prems, context} =>
+                InductTacs.case_tac (context |> Variable.declare_term y) ("y", NONE) 1 THEN
+                asm_simp_tac (HOL_basic_ss addsimps simp1) 1 THEN
+                rtac @{thm exI} 1 THEN
+                rtac @{thm refl} 1
 
               (* third statement *)
               val (inject_thm,thy3) =