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