# HG changeset patch
# User wenzelm
# Date 1266317773 -3600
# Node ID c8a6fae0ad0cdc6e373d6eeb4709e1cd808eec7c
# Parent  e1a226a191b60164b97eafa9a29c1d1bb059f72c
refrain from using @{const_name} in syntax translations;

diff -r e1a226a191b6 -r c8a6fae0ad0c src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Tue Feb 16 11:27:29 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Tue Feb 16 11:56:13 2010 +0100
@@ -146,7 +146,7 @@
                         (replicate (length rstp) "x")
                     in
                       [((prfx, gvars @ map Free (xs ~~ Ts)),
-                        (Const (@{const_name HOL.undefined}, res_ty), (~1, false)))]
+                        (Const (@{const_syntax undefined}, res_ty), (~1, false)))]
                     end
                   else in_group
               in
@@ -315,7 +315,7 @@
       fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
             let val (t', used') = prep_pat t used
             in (c $ t' $ tT, used') end
-        | prep_pat (Const (@{const_name dummy_pattern}, T)) used =
+        | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
             let val x = Name.variant used "x"
             in (Free (x, T), x :: used) end
         | prep_pat (Const (s, T)) used =
@@ -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_name HOL.undefined});
+        val is_undefined = name_of #> equal (SOME @{const_syntax 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_name dummy_pattern}, R)
+                  if d then Const (@{const_syntax 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