--- 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
--- a/src/HOL/Tools/Function/function_core.ML Sun Jul 05 15:02:30 2015 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Sun Jul 05 15:43:45 2015 +0200
@@ -15,7 +15,7 @@
-> local_theory
-> (term (* f *)
* thm (* goalstate *)
- * (thm -> Function_Common.function_result) (* continuation *)
+ * (Proof.context -> thm -> Function_Common.function_result) (* continuation *)
) * local_theory
end
@@ -893,11 +893,8 @@
(prove_stuff lthy globals G f R xclauses complete compat
compat_store G_elim) f_defthm
- fun mk_partial_rules provedgoal =
+ fun mk_partial_rules newctxt provedgoal =
let
- val newthy = Thm.theory_of_thm provedgoal (*FIXME*)
- val newctxt = Proof_Context.init_global newthy (*FIXME*)
-
val (graph_is_function, complete_thm) =
provedgoal
|> Conjunction.elim
--- a/src/HOL/Tools/Function/mutual.ML Sun Jul 05 15:02:30 2015 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Sun Jul 05 15:43:45 2015 +0200
@@ -12,7 +12,7 @@
-> term list
-> local_theory
-> ((thm (* goalstate *)
- * (thm -> Function_Common.function_result) (* proof continuation *)
+ * (Proof.context -> thm -> Function_Common.function_result) (* proof continuation *)
) * local_theory)
end
@@ -310,7 +310,7 @@
val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
- val cont' = mk_partial_rules_mutual lthy'' cont mutual'
+ fun cont' ctxt = mk_partial_rules_mutual lthy'' (cont ctxt) mutual'
in
((goalstate, cont'), lthy'')
end