138 let |
138 let |
139 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
139 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
140 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
140 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
141 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
141 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
142 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
142 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
143 val (eqs, post, sort_cont, cnames) = empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *) |
143 val (eqs, post, sort_cont, cnames) = |
|
144 empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *) |
144 |
145 |
145 val defname = mk_defname fixes |
146 val defname = mk_defname fixes |
146 val FunctionConfig {partials, default, ...} = config |
147 val FunctionConfig {partials, default, ...} = config |
147 val _ = |
148 val _ = |
148 if is_some default then Output.legacy_feature |
149 if is_some default then Output.legacy_feature |