src/Pure/Tools/codegen_serializer.ML

     val tab =
       Symtab.empty
       |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
            o fst o dest_name o fst)
              code
-  in (fn name => (the o Symtab.lookup tab) name) end;
+  in fn name => (the o Symtab.lookup tab) name end;
 
 
 
 (** SML/OCaml serializer **)
 

             fun pr ((v, pat), ty) =
               pr_bind NOBR ((SOME v, pat), ty)
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (ps @ [pr_term vars' NOBR t']) end
-      | pr_term vars fxy (t as ICase (_, [_])) =
-          let
-            val (binds, t') = CodegenThingol.unfold_let t;
-            fun pr ((pat, ty), t) vars =
-              vars
-              |> pr_bind NOBR ((NONE, SOME pat), ty)
-              |>> (fn p => semicolon [str "val", p, str "=", pr_term vars NOBR t])
-            val (ps, vars') = fold_map pr binds vars;
-          in
-            Pretty.chunks [
-              [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
-              [str ("in"), Pretty.fbrk, pr_term vars' NOBR t'] |> Pretty.block,
-              str ("end")
-            ]
-          end
-      | pr_term vars fxy (ICase ((td, ty), b::bs)) =
-          let
-            fun pr delim (pat, t) =
-              let
-                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
-              in
-                concat [str delim, p, str "=>", pr_term vars' NOBR t]
-              end;
-          in
-            (Pretty.enclose "(" ")" o single o brackify fxy) (
-              str "case"
-              :: pr_term vars NOBR td
-              :: pr "of" b
-              :: map (pr "|") bs
-            )
-          end
-      | pr_term vars fxy (t as ICase (_, [])) = str "raise Fail \"empty case\""
+      | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
+                then pr_case vars fxy cases
+                else pr_app vars fxy c_ts
+            | NONE => pr_case vars fxy cases)
     and pr_app' vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then let
         val k = length tys
       in if k < 2 then 
         (str o deresolv) c :: map (pr_term vars BR) ts

     and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
     and pr_bind' ((NONE, NONE), _) = str "_"
       | pr_bind' ((SOME v, NONE), _) = str v
       | pr_bind' ((NONE, SOME p), _) = p
       | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
-    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
+    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
+    and pr_case vars fxy (cases as ((_, [_]), _)) =
+          let
+            val (binds, t') = CodegenThingol.unfold_let (ICase cases);
+            fun pr ((pat, ty), t) vars =
+              vars
+              |> pr_bind NOBR ((NONE, SOME pat), ty)
+              |>> (fn p => semicolon [str "val", p, str "=", pr_term vars NOBR t])
+            val (ps, vars') = fold_map pr binds vars;
+          in
+            Pretty.chunks [
+              [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
+              [str ("in"), Pretty.fbrk, pr_term vars' NOBR t'] |> Pretty.block,
+              str ("end")
+            ]
+          end
+      | pr_case vars fxy (((td, ty), b::bs), _) =
+          let
+            fun pr delim (pat, t) =
+              let
+                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
+              in
+                concat [str delim, p, str "=>", pr_term vars' NOBR t]
+              end;
+          in
+            (Pretty.enclose "(" ")" o single o brackify fxy) (
+              str "case"
+              :: pr_term vars NOBR td
+              :: pr "of" b
+              :: map (pr "|") bs
+            )
+          end
+      | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\""
     fun pr_def (MLFuns (funns as (funn :: funns'))) =
           let
             val definer =
               let
                 fun mk [] [] = "val"

           let
             val (binds, t') = CodegenThingol.unfold_abs t;
             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (str "fun" :: ps @ str "->" @@ pr_term vars' NOBR t') end
-      | pr_term vars fxy (t as ICase (_, [_])) =
-          let
-            val (binds, t') = CodegenThingol.unfold_let t;
-            fun pr ((pat, ty), t) vars =
-              vars
-              |> pr_bind NOBR ((NONE, SOME pat), ty)
-              |>> (fn p => concat [str "let", p, str "=", pr_term vars NOBR t, str "in"])
-            val (ps, vars') = fold_map pr binds vars;
-          in Pretty.chunks (ps @| pr_term vars' NOBR t') end
-      | pr_term vars fxy (ICase ((td, ty), b::bs)) =
-          let
-            fun pr delim (pat, t) =
-              let
-                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
-              in concat [str delim, p, str "->", pr_term vars' NOBR t] end;
-          in
-            (Pretty.enclose "(" ")" o single o brackify fxy) (
-              str "match"
-              :: pr_term vars NOBR td
-              :: pr "with" b
-              :: map (pr "|") bs
-            )
-          end
-      | pr_term vars fxy (t as ICase (_, [])) = str "failwith \"empty case\""
+      | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
+                then pr_case vars fxy cases
+                else pr_app vars fxy c_ts
+            | NONE => pr_case vars fxy cases)
     and pr_app' vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then
         if length tys = length ts
         then case ts
          of [] => [(str o deresolv) c]

     and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
     and pr_bind' ((NONE, NONE), _) = str "_"
       | pr_bind' ((SOME v, NONE), _) = str v
       | pr_bind' ((NONE, SOME p), _) = p
       | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
-    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
+    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
+    and pr_case vars fxy (cases as ((_, [_]), _)) =
+          let
+            val (binds, t') = CodegenThingol.unfold_let (ICase cases);
+            fun pr ((pat, ty), t) vars =
+              vars
+              |> pr_bind NOBR ((NONE, SOME pat), ty)
+              |>> (fn p => concat [str "let", p, str "=", pr_term vars NOBR t, str "in"])
+            val (ps, vars') = fold_map pr binds vars;
+          in Pretty.chunks (ps @| pr_term vars' NOBR t') end
+      | pr_case vars fxy (((td, ty), b::bs), _) =
+          let
+            fun pr delim (pat, t) =
+              let
+                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
+              in concat [str delim, p, str "->", pr_term vars' NOBR t] end;
+          in
+            (Pretty.enclose "(" ")" o single o brackify fxy) (
+              str "match"
+              :: pr_term vars NOBR td
+              :: pr "with" b
+              :: map (pr "|") bs
+            )
+          end
+      | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\"";
     fun pr_def (MLFuns (funns as funn :: funns')) =
           let
             fun fish_parm _ (w as SOME _) = w
               | fish_parm (IVar v) NONE = SOME v
               | fish_parm _ NONE = NONE;

           let
             val (binds, t') = CodegenThingol.unfold_abs t;
             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (str "\\" :: ps @ str "->" @@ pr_term vars' NOBR t') end
-      | pr_term vars fxy (t as ICase (_, [_])) =
-          let
-            val (binds, t) = CodegenThingol.unfold_let t;
+      | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
+                then pr_case vars fxy cases
+                else pr_app vars fxy c_ts
+            | NONE => pr_case vars fxy cases)
+    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
+    and pr_bind fxy = pr_bind_haskell pr_term fxy
+    and pr_case vars fxy (cases as ((_, [_]), _)) =
+          let
+            val (binds, t) = CodegenThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
               |> pr_bind BR ((NONE, SOME pat), ty)
               |>> (fn p => semicolon [p, str "=", pr_term vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;

             Pretty.block_enclose (
               str "let {",
               concat [str "}", str "in", pr_term vars' NOBR t]
             ) ps
           end
-      | pr_term vars fxy (ICase ((td, ty), bs as _ :: _)) =
+      | pr_case vars fxy (((td, ty), bs as _ :: _), _) =
           let
             fun pr (pat, t) =
               let
                 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
               in semicolon [p, str "->", pr_term vars' NOBR t] end;

             Pretty.block_enclose (
               concat [str "(case", pr_term vars NOBR td, str "of", str "{"],
               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
-    and pr_bind fxy = pr_bind_haskell pr_term fxy;
+      | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";
     fun pr_def (name, CodegenThingol.Fun (eqs, (vs, ty))) =
           let
             val tyvars = CodegenNames.intro_vars (map fst vs) init_syms;
             fun pr_eq (ts, t) =
               let

 
 val pretty_imperative_monad_bind =
   let
     fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T)
           vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
-            pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
+            pr vars fxy (ICase (((t1, ty), ([(IVar v, t2)])), IVar ""))
       | pretty pr vars fxy [(t1, _), (t2, ty2)] =
           let
             (*this code suffers from the lack of a proper concept for bindings*)
             val vs = CodegenThingol.fold_varnames cons t2 [];
             val v = Name.variant vs "x";
             val vars' = CodegenNames.intro_vars [v] vars;
             val var = IVar v;
             val ty = (hd o fst o CodegenThingol.unfold_fun) ty2;
-          in pr vars' fxy (ICase ((t1, ty), ([(var, t2 `$ var)]))) end;
+          in pr vars' fxy (ICase (((t1, ty), ([(var, t2 `$ var)])), IVar "")) end;
   in (2, pretty) end;
 
 end; (*local*)
 
 (** ML and Isar interface **)

         str "->",
         pr_typ (INFX (1, R)) ty2
       ]))
   #> fold (add_reserved "SML") ML_Syntax.reserved_names
   #> fold (add_reserved "SML")
-      ["o" (*dictionary projections use it already*), "div", "mod" (*standard infixes*)]
+      ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
   #> fold (add_reserved "OCaml") [
       "and", "as", "assert", "begin", "class",
       "constraint", "do", "done", "downto", "else", "end", "exception",
       "external", "false", "for", "fun", "function", "functor", "if",
       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
       "sig", "struct", "then", "to", "true", "try", "type", "val",
-      "virtual", "when", "while", "with", "mod"
+      "virtual", "when", "while", "with"
     ]
+  #> fold (add_reserved "OCaml") ["failwith", "mod"]
   #> fold (add_reserved "Haskell") [
       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
       "import", "default", "forall", "let", "in", "class", "qualified", "data",
       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
     ]