# HG changeset patch
# User wenzelm
# Date 1436103825 -7200
# Node ID 9173467ec5b6074a9188cc75d6ed5f2b7cb1a293
# Parent  48dd1cefb4ae155252731eb8cd89fb926db50d2a
clarified context;

diff -r 48dd1cefb4ae -r 9173467ec5b6 src/HOL/Tools/Function/function.ML
--- 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
 
diff -r 48dd1cefb4ae -r 9173467ec5b6 src/HOL/Tools/Function/function_core.ML
--- 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
diff -r 48dd1cefb4ae -r 9173467ec5b6 src/HOL/Tools/Function/mutual.ML
--- 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