equal
deleted
inserted
replaced
149 |
149 |
150 fun afterqed [[proof]] lthy = |
150 fun afterqed [[proof]] lthy = |
151 let |
151 let |
152 val NominalFunctionResult {fs, R, psimps, simple_pinducts, |
152 val NominalFunctionResult {fs, R, psimps, simple_pinducts, |
153 termination, domintros, cases, eqvts, ...} = |
153 termination, domintros, cases, eqvts, ...} = |
154 cont (Thm.close_derivation proof) |
154 cont lthy (Thm.close_derivation proof) |
155 |
155 |
156 val fnames = map (fst o fst) fixes |
156 val fnames = map (fst o fst) fixes |
157 fun qualify n = Binding.name n |
157 fun qualify n = Binding.name n |
158 |> Binding.qualify true defname |
158 |> Binding.qualify true defname |
159 val concealed_partial = if partials then I else Binding.concealed |
159 val concealed_partial = if partials then I else Binding.concealed |
212 val ((goal_state, afterqed), lthy') = |
212 val ((goal_state, afterqed), lthy') = |
213 prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy |
213 prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy |
214 in |
214 in |
215 lthy' |
215 lthy' |
216 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]] |
216 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]] |
217 |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd |
217 |> Proof.refine_singleton (Method.primitive_text (K (K goal_state))) |
218 end |
218 end |
219 |
219 |
220 val nominal_function = |
220 val nominal_function = |
221 gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type}) |
221 gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type}) |
222 fun nominal_function_cmd a b c int = |
222 fun nominal_function_cmd a b c int = |