changeset 59826 | 442b09c0f898 |
parent 59802 | 684cfaa12e47 |
child 59936 | b8ffc3dc9e24 |
--- a/src/HOL/Nominal/nominal_atoms.ML Fri Mar 27 11:38:26 2015 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Fri Mar 27 17:46:08 2015 +0100 @@ -131,7 +131,7 @@ (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0))) val proof2 = fn {prems, context = ctxt} => - Induct_Tacs.case_tac ctxt "y" [] 1 THEN + Induct_Tacs.case_tac ctxt "y" [] NONE 1 THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1 THEN rtac @{thm exI} 1 THEN rtac @{thm refl} 1