equal
deleted
inserted
replaced
92 fun register_fp_sugar key fp_sugar = |
92 fun register_fp_sugar key fp_sugar = |
93 Local_Theory.declaration {syntax = false, pervasive = true} |
93 Local_Theory.declaration {syntax = false, pervasive = true} |
94 (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); |
94 (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); |
95 |
95 |
96 fun register_fp_sugars lfp pre_bnfs (fp_res as {ctors, ...}) ctr_sugars xxfolds xxrecs lthy = |
96 fun register_fp_sugars lfp pre_bnfs (fp_res as {ctors, ...}) ctr_sugars xxfolds xxrecs lthy = |
97 (1, lthy) |
97 (0, lthy) |
98 |> fold (fn ctor => fn (kk, lthy) => (kk + 1, |
98 |> fold (fn ctor => fn (kk, lthy) => (kk + 1, |
99 register_fp_sugar (fp_name_of_ctor ctor) {lfp = lfp, index = kk, |
99 register_fp_sugar (fp_name_of_ctor ctor) {lfp = lfp, index = kk, |
100 pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugars = ctr_sugars, xxfolds = xxfolds, |
100 pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugars = ctr_sugars, xxfolds = xxfolds, |
101 xxrecs = xxrecs} lthy)) ctors |
101 xxrecs = xxrecs} lthy)) ctors |
102 |> snd; |
102 |> snd; |