# HG changeset patch
# User haftmann
# Date 1242137496 -7200
# Node ID f79a0d03b75f4027545a172fbee61c510af8893a
# Parent  379378d59b08e0a1493808776b82373fa7b088e3
tuned exception code

diff -r 379378d59b08 -r f79a0d03b75f src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Mon May 11 21:55:30 2009 -0700
+++ b/src/Tools/code/code_ml.ML	Tue May 12 16:11:36 2009 +0200
@@ -161,20 +161,21 @@
               :: map (pr "|") clauses
             )
           end
-      | pr_case is_closure thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
+      | pr_case is_closure thm vars fxy ((_, []), _) =
+          (concat o map str) ["raise", "Fail", "\"empty case\""];
     fun pr_stmt (MLExc (name, n)) =
           let
             val exc_str =
               (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
           in
-            concat (
-              str (if n = 0 then "val" else "fun")
-              :: (str o deresolve) name
-              :: map str (replicate n "_")
-              @ str "="
-              :: str "raise"
-              :: str "(Fail"
-              @@ str (exc_str ^ ")")
+            (concat o map str) (
+              (if n = 0 then "val" else "fun")
+              :: deresolve name
+              :: replicate n "_"
+              @ "="
+              :: "raise"
+              :: "Fail"
+              @@ exc_str
             )
           end
       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
@@ -458,7 +459,8 @@
               :: map (pr "|") clauses
             )
           end
-      | pr_case is_closure thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
+      | pr_case is_closure thm vars fxy ((_, []), _) =
+          (concat o map str) ["failwith", "\"empty case\""];
     fun fish_params vars eqs =
       let
         fun fish_param _ (w as SOME _) = w
@@ -477,13 +479,13 @@
             val exc_str =
               (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
           in
-            concat (
-              str "let"
-              :: (str o deresolve) name
-              :: map str (replicate n "_")
-              @ str "="
-              :: str "failwith"
-              @@ str exc_str
+            (concat o map str) (
+              "let"
+              :: deresolve name
+              :: replicate n "_"
+              @ "="
+              :: "failwith"
+              @@ exc_str
             )
           end
       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =