# HG changeset patch
# User wenzelm
# Date 1267222125 -3600
# Node ID 5da5ac6c6b771b76b14ea183058cad33845c8db7
# Parent  34d8e0a9bfa7409629d04ee41658b57ee09a2eb0
gen_dest_case: recovered @{const_name} from c8a6fae0ad0c, because of separate Syntax.mark_const in case_tr' -- avoid extra syntax markers in output;

diff -r 34d8e0a9bfa7 -r 5da5ac6c6b77 src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Fri Feb 26 23:07:27 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Fri Feb 26 23:08:45 2010 +0100
@@ -381,7 +381,7 @@
         fun count_cases (_, _, true) = I
           | count_cases (c, (_, body), false) =
               AList.map_default op aconv (body, []) (cons c);
-        val is_undefined = name_of #> equal (SOME @{const_syntax undefined});
+        val is_undefined = name_of #> equal (SOME @{const_name undefined});
         fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body)
       in case ty_info tab cname of
           SOME {constructors, case_name} =>
@@ -399,7 +399,7 @@
                   (fold_rev count_cases cases []);
                 val R = type_of t;
                 val dummy =
-                  if d then Const (@{const_syntax dummy_pattern}, R)
+                  if d then Const (@{const_name dummy_pattern}, R)
                   else Free (Name.variant used "x", R)
               in
                 SOME (x, map mk_case (case find_first (is_undefined o fst) cases' of