140 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
140 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
141 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
141 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
142 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
142 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
143 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
143 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
144 val (eqs, post, sort_cont, cnames) = |
144 val (eqs, post, sort_cont, cnames) = |
145 empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *) |
145 empty_preproc nominal_check_defs (Function_Common.default_config) ctxt' fixes spec (* nominal *) |
146 |
146 |
147 val defname = mk_defname fixes |
147 val defname = mk_defname fixes |
148 val NominalFunctionConfig {partials, ...} = config |
148 val NominalFunctionConfig {partials, ...} = config |
149 |
149 |
150 val ((goal_state, cont), lthy') = |
150 val ((goal_state, cont), lthy') = |