equal
deleted
inserted
replaced
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] = |