equal
deleted
inserted
replaced
78 (saved_simps, fold2 add_for_f fnames simps_by_f lthy) |
78 (saved_simps, fold2 add_for_f fnames simps_by_f lthy) |
79 end |
79 end |
80 |
80 |
81 fun prepare_function do_print prep fixspec eqns config lthy = |
81 fun prepare_function do_print prep fixspec eqns config lthy = |
82 let |
82 let |
83 val ((fixes0, spec0), ctxt') = |
83 val ((fixes0, spec0), ctxt') = prep fixspec eqns lthy; |
84 lthy |
|
85 |> Proof_Context.set_object_logic_constraint |
|
86 |> prep fixspec eqns |
|
87 ||> Proof_Context.restore_object_logic_constraint lthy; |
|
88 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
84 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
89 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
85 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
90 val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
86 val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
91 |
87 |
92 val defname = mk_defname fixes |
88 val defname = mk_defname fixes |