src/Pure/Syntax/printer.ML

   mapfilter (fn mode => assoc (prtabs, mode)) (modes @ [""]);
 
 
 (* xprod_to_fmt *)
 
-fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = None
+fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = NONE
   | xprod_to_fmt (SynExt.XProd (_, xsymbs, const, pri)) =
       let
         fun cons_str s (String s' :: syms) = String (s ^ s') :: syms
           | cons_str s syms = String s :: syms;
 

           | nargs (Break _ :: syms) = nargs syms
           | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
           | nargs [] = 0;
       in
         (case xsyms_to_syms xsymbs of
-          (symbs, []) => Some (const, (symbs, nargs symbs, pri))
+          (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
         | _ => sys_error "xprod_to_fmt: unbalanced blocks")
       end;
 
 
 (* empty, extend, merge prtabs *)

   let
     val trans = apply_trans "print ast translation";
 
     fun token_trans c [Ast.Variable x] =
           (case tokentrf c of
-            None => None
-          | Some f => Some (f x))
-      | token_trans _ _ = None;
+            NONE => NONE
+          | SOME f => SOME (f x))
+      | token_trans _ _ = NONE;
 
     (*default applications: prefix / postfix*)
     val appT =
       if type_mode then TypeExt.tappl_ast_tr'
       else if curried then SynTrans.applC_ast_tr'

               else if nargs > n andalso not type_mode then
                 astT (appT (splitT n ([c], args)), p)
               else prnt (prnps, tbs);
       in
         (case token_trans a args of     (*try token translation function*)
-          Some s_len => [Pretty.raw_str s_len]
-        | None =>                       (*try print translation functions*)
+          SOME s_len => [Pretty.raw_str s_len]
+        | NONE =>                       (*try print translation functions*)
             astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
       end
 
     and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
       | astT (Ast.Variable x, _) = [Pretty.str x]