# HG changeset patch
# User wenzelm
# Date 1213478409 -7200
# Node ID dc1455f96f56d953b5d5ab79f1e242495fb3db57
# Parent  b43785a81e0112d702d106865bb941f2d3cfc756
InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;

diff -r b43785a81e01 -r dc1455f96f56 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Jun 14 23:20:07 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Jun 14 23:20:09 2008 +0200
@@ -95,7 +95,7 @@
                   (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
 
               val proof2 = fn {prems, context} =>
-                InductTacs.case_tac (context |> Variable.declare_term y) ("y", NONE) 1 THEN
+                InductTacs.case_tac context "y" 1 THEN
                 asm_simp_tac (HOL_basic_ss addsimps simp1) 1 THEN
                 rtac @{thm exI} 1 THEN
                 rtac @{thm refl} 1