# HG changeset patch
# User wenzelm
# Date 1326299434 -3600
# Node ID 8297006abc13ea425dce8fe4949153f694d3d3d4
# Parent  f009e0fe86438dab613c7ecebb0de7db208c770c
actually try to preserve names given by user (cf. 463b594e186a);

diff -r f009e0fe8643 -r 8297006abc13 src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Wed Jan 11 16:47:30 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Wed Jan 11 17:30:34 2012 +0100
@@ -63,7 +63,7 @@
   let
     val name' = if name = "" then (case t of Free (name', _) => name' | _ => name) else name;
     val cs' = if is_Free t then cs else filter_out Term_Position.is_position cs;
-  in (name, cs') end;
+  in (name', cs') end;
 
 fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
       strip_constraints t ||> cons tT