Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nominal/nominal_atoms.ML
changeset 59802 684cfaa12e47
parent 59498 50b60f501b05
child 59826 442b09c0f898 
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 24 20:07:27 2015 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 24 21:54:25 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" [] 1 THEN
                 asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1 THEN
                 rtac @{thm exI} 1 THEN
                 rtac @{thm refl} 1
isabelle