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/Datatype/datatype_case.ML
changeset 45156 a9b6c2ea7bec
parent 44121 44adaa6db327
child 45700 9dcbf6a1829c 
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Sun Oct 16 16:56:01 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Sun Oct 16 18:48:30 2011 +0200
@@ -346,7 +346,7 @@
                   (fold_rev count_cases cases []);
                 val R = type_of t;
                 val dummy =
-                  if d then Const (@{const_name dummy_pattern}, R)
+                  if d then Term.dummy_pattern R
                   else Free (singleton (Name.variant_list used) "x", R);
               in
                 SOME (x,
isabelle