equal
deleted
inserted
replaced
85 if is_some default |
85 if is_some default |
86 then legacy_feature "\"function (default)\" -- use 'partial_function' instead" |
86 then legacy_feature "\"function (default)\" -- use 'partial_function' instead" |
87 else () |
87 else () |
88 |
88 |
89 val ((goal_state, cont), lthy') = |
89 val ((goal_state, cont), lthy') = |
90 Function_Mutual.prepare_function_mutual config defname fixes eqs lthy |
90 Function_Mutual.prepare_function_mutual config defname fixes0 eqs lthy |
91 |
91 |
92 fun afterqed [[proof]] lthy = |
92 fun afterqed [[proof]] lthy = |
93 let |
93 let |
94 val result = cont lthy (Thm.close_derivation proof) |
94 val result = cont lthy (Thm.close_derivation proof) |
95 val FunctionResult {fs, R, dom, psimps, simple_pinducts, |
95 val FunctionResult {fs, R, dom, psimps, simple_pinducts, |