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/Tools/Function/scnp_reconstruct.ML
changeset 55642 63beb38e9258
parent 54998 8601434fa334
child 57959 1bfed12a7646 
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -129,7 +129,7 @@
   THEN rtac @{thm CollectI} 1
   THEN etac @{thm conjE} 1
   THEN etac @{thm ssubst} 1
-  THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.cases}
+  THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.case}
 
 (* Sets *)
isabelle