src/HOLCF/ax_ops/thy_ops.ML

 in
 (* the following is an adapted version of const_decls from thy_parse.ML *)
 
 val names1 = list1 name;
 
-val split_decls = flat o map (fn (xs, y) => map (rpair y) xs);
+fun split_decls decls = flat (map (fn (xs, y) => map (rpair y) xs) decls);
 
 fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
 
 fun mk_strict_vals [] = ""
   | mk_strict_vals [name] =