# HG changeset patch
# User wenzelm
# Date 1325859557 -3600
# Node ID 6bff2ebaf7bbbceb2194fea0e685f1ed4c5d309d
# Parent  4b9d4659228a22068f134b2d9f09595a51463530
more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);

diff -r 4b9d4659228a -r 6bff2ebaf7bb src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Fri Jan 06 11:27:49 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Fri Jan 06 15:19:17 2012 +0100
@@ -4,8 +4,15 @@
 
 Datatype package: nested case expressions on datatypes.
 
-TODO: generic tool with separate data slot, without hard-wiring the
-datatype package.
+TODO:
+  * Avoid fragile operations on syntax trees (with type constraints
+    getting in the way).  Instead work with auxiliary "destructor"
+    constants in translations and introduce the actual case
+    combinators in a separate term check phase (similar to term
+    abbreviations).
+
+  * Avoid hard-wiring with datatype package.  Instead provide generic
+    generic declarations of case splits based on an internal data slot.
 *)
 
 signature DATATYPE_CASE =
@@ -60,6 +67,9 @@
       strip_constraints t ||> cons tT
   | strip_constraints t = (t, []);
 
+val recover_constraints =
+  fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT);
+
 fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
 
 
@@ -302,8 +312,8 @@
       in
         make_case_untyped ctxt
           (if err then Error else Warning) []
-          (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
-             (flat cnstrts) t) cases
+          (recover_constraints (filter_out Term_Position.is_position (flat cnstrts)) t)
+          cases
       end
   | case_tr _ _ _ = case_error "case_tr";