97 fun gen_add_fundef is_external prep default_constraint fixspec eqnss config flags lthy = |
97 fun gen_add_fundef is_external prep default_constraint fixspec eqnss config flags lthy = |
98 let |
98 let |
99 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
99 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
100 val ((fixes0, spec0), ctxt') = |
100 val ((fixes0, spec0), ctxt') = |
101 prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy |
101 prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy |
102 val fixes = map (apfst (apfst Binding.base_name)) fixes0; |
102 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
103 val spec = map (apfst (apfst Binding.base_name)) spec0; |
103 val spec = map (apfst (apfst Binding.name_of)) spec0; |
104 val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec |
104 val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec |
105 |
105 |
106 val defname = mk_defname fixes |
106 val defname = mk_defname fixes |
107 |
107 |
108 val ((goalstate, cont), lthy) = |
108 val ((goalstate, cont), lthy) = |