--- a/src/HOL/Tools/datatype_package.ML Fri Jul 21 11:34:01 2006 +0200
+++ b/src/HOL/Tools/datatype_package.ML Fri Jul 21 14:11:14 2006 +0200
@@ -431,10 +431,12 @@
val (_, (_, dts, constrs)) = List.nth (descr, index);
fun find_case (cases, (s, dt)) =
(case find_first (equal s o fst o fst) cases' of
- NONE => (case default of
- NONE => case_error ("No clause for constructor " ^ s) (SOME tname) [u]
- | SOME t => (cases, list_abs (map (rpair dummyT) (DatatypeProp.make_tnames
- (map (typ_of_dtyp descr sorts) dt)), t)))
+ NONE => (cases, list_abs (map (rpair dummyT)
+ (DatatypeProp.make_tnames (map (typ_of_dtyp descr sorts) dt)),
+ case default of
+ NONE => (warning ("No clause for constructor " ^ s ^
+ " in case expression"); Const ("undefined", dummyT))
+ | SOME t => t))
| SOME (c as ((_, vs), t)) =>
if length dt <> length vs then
case_error ("Wrong number of arguments for constructor " ^ s)
@@ -484,10 +486,16 @@
(Library.foldl count_cases ([], cases));
fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
list_comb (Syntax.const cname, vs) $ body;
+ fun is_undefined (Const ("undefined", _)) = true
+ | is_undefined _ = false;
in
Syntax.const "_case_syntax" $ x $
foldr1 (fn (t, u) => Syntax.const "_case2" $ t $ u) (map mk_case1
- (case cases' of
+ (case find_first (is_undefined o fst) cases' of
+ SOME (_, cnames) =>
+ if length cnames = length constrs then [hd cases]
+ else filter_out (fn (_, (_, body), _) => is_undefined body) cases
+ | NONE => case cases' of
[] => cases
| (default, cnames) :: _ =>
if length cnames = 1 then cases