src/HOL/Nominal/nominal_atoms.ML
changeset 45133 2214ba5bdfff
parent 44689 f247fc952f31
child 45701 615da8b8d758
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Oct 12 22:21:38 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Oct 12 22:48:23 2011 +0200
     1.3 @@ -132,7 +132,7 @@
     1.4                    (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
     1.5  
     1.6                val proof2 = fn {prems, context} =>
     1.7 -                InductTacs.case_tac context "y" 1 THEN
     1.8 +                Induct_Tacs.case_tac context "y" 1 THEN
     1.9                  asm_simp_tac (HOL_basic_ss addsimps simp1) 1 THEN
    1.10                  rtac @{thm exI} 1 THEN
    1.11                  rtac @{thm refl} 1