src/HOLCF/ax_ops/thy_ops.ML
changeset 2238 c72a23bbe762
parent 1810 0eef167ebe1b
child 3534 c245c88194ff
equal deleted inserted replaced
2237:f01ac387e82b 2238:c72a23bbe762
   369 in
   369 in
   370 (* the following is an adapted version of const_decls from thy_parse.ML *)
   370 (* the following is an adapted version of const_decls from thy_parse.ML *)
   371 
   371 
   372 val names1 = list1 name;
   372 val names1 = list1 name;
   373 
   373 
   374 val split_decls = flat o map (fn (xs, y) => map (rpair y) xs);
   374 fun split_decls decls = flat (map (fn (xs, y) => map (rpair y) xs) decls);
   375 
   375 
   376 fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
   376 fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
   377 
   377 
   378 fun mk_strict_vals [] = ""
   378 fun mk_strict_vals [] = ""
   379   | mk_strict_vals [name] =
   379   | mk_strict_vals [name] =