# 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