--- 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