# HG changeset patch
# User haftmann
# Date 1174639257 -3600
# Node ID c5929d4373a073c1b028ce64a483ad2f7ded0d7f
# Parent  6ee2edbce31cd4796c1a2fa8f5502949a17aa5d4
added empty cases

diff -r 6ee2edbce31c -r c5929d4373a0 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Fri Mar 23 09:40:53 2007 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Fri Mar 23 09:40:57 2007 +0100
@@ -412,6 +412,7 @@
               :: map (pr "|") bs
             )
           end
+      | pr_term vars fxy (t as ICase (_, [])) = str "raise Fail \"empty case\""
     and pr_app' vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then let
         val k = length tys
@@ -681,6 +682,7 @@
               :: map (pr "|") bs
             )
           end
+      | pr_term vars fxy (t as ICase (_, [])) = str "failwith \"empty case\""
     and pr_app' vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then
         if length tys = length ts
@@ -1176,7 +1178,7 @@
               concat [str "}", str "in", pr_term vars' NOBR t]
             ) ps
           end
-      | pr_term vars fxy (ICase ((td, ty), bs)) =
+      | pr_term vars fxy (ICase ((td, ty), bs as _ :: _)) =
           let
             fun pr (pat, t) =
               let
@@ -1188,6 +1190,7 @@
               str "})"
             ) (map pr bs)
           end
+      | pr_term vars fxy (t as ICase (_, [])) = str "error \"empty case\""
     and pr_app' vars ((c, _), ts) =
       (str o deresolv) c :: map (pr_term vars BR) ts
     and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars