equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 signature NOMINAL_PRIMREC = |
9 signature NOMINAL_PRIMREC = |
10 sig |
10 sig |
11 val add_primrec: string -> string list option -> string option -> |
11 val add_primrec: string -> string list option -> string option -> |
12 ((bstring * string) * Attrib.src list) list -> theory -> Proof.state |
12 ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state |
13 val add_primrec_unchecked: string -> string list option -> string option -> |
13 val add_primrec_unchecked: string -> string list option -> string option -> |
14 ((bstring * string) * Attrib.src list) list -> theory -> Proof.state |
14 ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state |
15 val add_primrec_i: string -> term list option -> term option -> |
15 val add_primrec_i: string -> term list option -> term option -> |
16 ((bstring * term) * attribute list) list -> theory -> Proof.state |
16 ((Name.binding * term) * attribute list) list -> theory -> Proof.state |
17 val add_primrec_unchecked_i: string -> term list option -> term option -> |
17 val add_primrec_unchecked_i: string -> term list option -> term option -> |
18 ((bstring * term) * attribute list) list -> theory -> Proof.state |
18 ((Name.binding * term) * attribute list) list -> theory -> Proof.state |
19 end; |
19 end; |
20 |
20 |
21 structure NominalPrimrec : NOMINAL_PRIMREC = |
21 structure NominalPrimrec : NOMINAL_PRIMREC = |
22 struct |
22 struct |
23 |
23 |
227 |
227 |
228 local |
228 local |
229 |
229 |
230 fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy = |
230 fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy = |
231 let |
231 let |
232 val (eqns, atts) = split_list eqns_atts; |
232 val (raw_eqns, atts) = split_list eqns_atts; |
|
233 val eqns = map (apfst Name.name_of) raw_eqns; |
233 val dt_info = NominalPackage.get_nominal_datatypes thy; |
234 val dt_info = NominalPackage.get_nominal_datatypes thy; |
234 val rec_eqns = fold_rev (process_eqn thy o snd) eqns []; |
235 val rec_eqns = fold_rev (process_eqn thy o snd) eqns []; |
235 val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) => |
236 val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) => |
236 map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) rec_eqns |
237 map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) rec_eqns |
237 val _ = |
238 val _ = |