equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature FUNCTION_LIB = |
8 signature FUNCTION_LIB = |
9 sig |
9 sig |
10 val function_internals: bool Config.T |
10 val function_internals: bool Config.T |
|
11 |
|
12 val derived_name: binding -> string -> binding |
|
13 val name_suffix: binding -> string -> binding |
|
14 val derived_name_suffix: binding -> string -> binding |
11 |
15 |
12 val plural: string -> string -> 'a list -> string |
16 val plural: string -> string -> 'a list -> string |
13 |
17 |
14 val dest_all_all: term -> term list * term |
18 val dest_all_all: term -> term list * term |
15 |
19 |
31 |
35 |
32 structure Function_Lib: FUNCTION_LIB = |
36 structure Function_Lib: FUNCTION_LIB = |
33 struct |
37 struct |
34 |
38 |
35 val function_internals = Attrib.setup_config_bool @{binding function_internals} (K false) |
39 val function_internals = Attrib.setup_config_bool @{binding function_internals} (K false) |
|
40 |
|
41 fun derived_name binding name = |
|
42 Binding.reset_pos (Binding.qualify_name true binding name) |
|
43 |
|
44 fun name_suffix binding sffx = Binding.map_name (suffix sffx) binding |
|
45 fun derived_name_suffix binding sffx = Binding.reset_pos (name_suffix binding sffx) |
36 |
46 |
37 |
47 |
38 (* "The variable" ^ plural " is" "s are" vs *) |
48 (* "The variable" ^ plural " is" "s are" vs *) |
39 fun plural sg pl [x] = sg |
49 fun plural sg pl [x] = sg |
40 | plural sg pl _ = pl |
50 | plural sg pl _ = pl |