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 27095 c1c27955d7dd
parent 26820 2909150bd614
child 27112 661a74bafeb7 
--- a/src/HOL/Nominal/nominal_atoms.ML	Sun Jun 08 14:31:06 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Jun 09 17:07:08 2008 +0200
@@ -94,7 +94,7 @@
               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 [case_tac "y" 1,
+              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]
isabelle