changeset 60643 | 9173467ec5b6 |
parent 60499 | 54a3db2ed201 |
child 61112 | e966c311e9a7 |
--- a/src/HOL/Tools/Function/function.ML Sun Jul 05 15:02:30 2015 +0200 +++ b/src/HOL/Tools/Function/function.ML Sun Jul 05 15:43:45 2015 +0200 @@ -98,7 +98,7 @@ fun afterqed [[proof]] lthy = let - val result = cont (Thm.close_derivation proof) + val result = cont lthy (Thm.close_derivation proof) val FunctionResult {fs, R, dom, psimps, simple_pinducts, termination, domintros, cases, ...} = result