74 val ((fixes0, spec0), ctxt') = prep fixspec eqns lthy |
74 val ((fixes0, spec0), ctxt') = prep fixspec eqns lthy |
75 val fixes = map (apfst (apfst Binding.name_of)) fixes0 |
75 val fixes = map (apfst (apfst Binding.name_of)) fixes0 |
76 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0 |
76 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0 |
77 val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
77 val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
78 val props0 = map snd spec0 |
78 val props0 = map snd spec0 |
79 val vars0 = map Term.strip_all_vars props0 |
79 fun varify (ps,prop) = |
80 val input_eqns = |
80 Term.subst_bounds (rev (map (fn (a,T) => Var((a,0),T)) ps), Term.strip_all_body prop) |
81 map (fn (ps,prop) => Term.subst_bounds (rev (map Free ps), Term.strip_all_body prop)) |
81 val input_eqns = map varify (map Term.strip_all_vars props0 ~~ props0) |
82 (vars0 ~~ props0) |
|
83 val fnames = map (fst o fst) fixes0 |
82 val fnames = map (fst o fst) fixes0 |
84 val defname = Binding.conglomerate fnames; |
83 val defname = Binding.conglomerate fnames; |
85 |
84 |
86 val FunctionConfig {partials, default, ...} = config |
85 val FunctionConfig {partials, default, ...} = config |
87 val _ = |
86 val _ = |