src/Tools/code/code_ml.ML
changeset 31121 f79a0d03b75f
parent 31063 88aaab83b6fc
child 31156 90fed3d4430f
     1.1 --- a/src/Tools/code/code_ml.ML	Mon May 11 21:55:30 2009 -0700
     1.2 +++ b/src/Tools/code/code_ml.ML	Tue May 12 16:11:36 2009 +0200
     1.3 @@ -161,20 +161,21 @@
     1.4                :: map (pr "|") clauses
     1.5              )
     1.6            end
     1.7 -      | pr_case is_closure thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
     1.8 +      | pr_case is_closure thm vars fxy ((_, []), _) =
     1.9 +          (concat o map str) ["raise", "Fail", "\"empty case\""];
    1.10      fun pr_stmt (MLExc (name, n)) =
    1.11            let
    1.12              val exc_str =
    1.13                (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
    1.14            in
    1.15 -            concat (
    1.16 -              str (if n = 0 then "val" else "fun")
    1.17 -              :: (str o deresolve) name
    1.18 -              :: map str (replicate n "_")
    1.19 -              @ str "="
    1.20 -              :: str "raise"
    1.21 -              :: str "(Fail"
    1.22 -              @@ str (exc_str ^ ")")
    1.23 +            (concat o map str) (
    1.24 +              (if n = 0 then "val" else "fun")
    1.25 +              :: deresolve name
    1.26 +              :: replicate n "_"
    1.27 +              @ "="
    1.28 +              :: "raise"
    1.29 +              :: "Fail"
    1.30 +              @@ exc_str
    1.31              )
    1.32            end
    1.33        | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
    1.34 @@ -458,7 +459,8 @@
    1.35                :: map (pr "|") clauses
    1.36              )
    1.37            end
    1.38 -      | pr_case is_closure thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
    1.39 +      | pr_case is_closure thm vars fxy ((_, []), _) =
    1.40 +          (concat o map str) ["failwith", "\"empty case\""];
    1.41      fun fish_params vars eqs =
    1.42        let
    1.43          fun fish_param _ (w as SOME _) = w
    1.44 @@ -477,13 +479,13 @@
    1.45              val exc_str =
    1.46                (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
    1.47            in
    1.48 -            concat (
    1.49 -              str "let"
    1.50 -              :: (str o deresolve) name
    1.51 -              :: map str (replicate n "_")
    1.52 -              @ str "="
    1.53 -              :: str "failwith"
    1.54 -              @@ str exc_str
    1.55 +            (concat o map str) (
    1.56 +              "let"
    1.57 +              :: deresolve name
    1.58 +              :: replicate n "_"
    1.59 +              @ "="
    1.60 +              :: "failwith"
    1.61 +              @@ exc_str
    1.62              )
    1.63            end
    1.64        | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =