tuned patterns;
authorwenzelm
Wed, 11 Dec 2013 20:38:39 +0100
changeset 54718 8c5221d698cd
parent 54717 42c209a6c225
child 54719 5cfcb7177988
tuned patterns;
src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Wed Dec 11 18:02:22 2013 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Dec 11 20:38:39 2013 +0100
@@ -131,7 +131,7 @@
 val pretty_ml =
   let
     fun convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (false, wd)
-      | convert _ (PolyML.PrettyBlock (ind, _,
+      | convert _ (PolyML.PrettyBlock (_, _,
             [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
           ML_Pretty.Break (true, 1)
       | convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
@@ -139,7 +139,7 @@
             fun property name default =
               (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
                 SOME (PolyML.ContextProperty (_, b)) => b
-              | NONE => default);
+              | _ => default);
             val bg = property "begin" "";
             val en = property "end" "";
             val len' = property "length" len;