src/HOL/Spec_Check/gen_construction.ML

 and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
 
 and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
   >> (fn (t, tl) => Tuple (t :: tl))) s;
 
-(*Parses entire type + name*)
+(*Parse entire type + name*)
 fun parse_function s =
   let
     val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
     val (name, ty) = p (split s)
     val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
     val (typ, _) = Scan.finite stop parse_type ty
   in (name, typ) end;
 
-(*Creates desired output*)
+(*Create desired output*)
 fun parse_pred s =
   let
     val (name, Con ("->", t :: _)) = parse_function s
   in (name, t) end;
 

   val empty = initial_content
   val extend = I
   fun merge data : T = Symtab.merge (K true) data
 )
 
-fun data_of thy tycon = case Symtab.lookup (Data.get thy) tycon of SOME data => data
-  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon)
+fun data_of thy tycon =
+  (case Symtab.lookup (Data.get thy) tycon of
+    SOME data => data
+  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
 
 val generator_of = fst oo data_of
 val printer_of = snd oo data_of
 
 fun register (ty, data) = Data.map (Symtab.update (ty, data))

       fun tuple_body t = space_implode " ^ \", \" ^ "
         (map (fn (ty, n) => "(" ^ compose_printer thy ty ^ ") x" ^ string_of_int n)
         (t ~~ (1 upto (length t))))
     in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
 
-(*produces compilable string*)
+(*produce compilable string*)
 fun build_check thy name (ty, spec) = "Spec_Check.checkGen (ML_Context.the_generic_context ()) ("
   ^ compose_generator thy ty ^ ", SOME (" ^ compose_printer thy ty ^ ")) (\""
   ^ name ^ "\", Property.pred (" ^ spec ^ "));";
 
-(*produces compilable string - non-eqtype functions*)
+(*produce compilable string - non-eqtype functions*)
 (*
 fun safe_check name (ty, spec) =
   let
     val default = case AList.lookup (op =) (!gen_table) "->"
       of NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")