diff -r 52a0a526e677 -r 0aefb31e27e0 src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Mon Sep 16 17:04:28 2013 +0200
+++ b/src/HOL/Tools/Function/function_elims.ML	Mon Sep 16 17:13:38 2013 +0200
@@ -14,7 +14,7 @@
 signature FUNCTION_ELIMS =
 sig
   val dest_funprop : term -> (term * term list) * term
-  val mk_partial_elim_rules : local_theory ->
+  val mk_partial_elim_rules : Proof.context ->
     Function_Common.function_result -> thm list list
 end;
 
@@ -74,8 +74,11 @@
 
 in
 
-fun mk_partial_elim_rules ctxt result=
-  let val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
+fun mk_partial_elim_rules ctxt result =
+  let
+      val thy = Proof_Context.theory_of ctxt;
+
+      val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
                           termination, domintros, ...} = result;
       val n_fs = length fs;
 
@@ -105,7 +108,6 @@
 
             val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
 
-            val thy = Proof_Context.theory_of ctxt;
             val cprop = cterm_of thy prop
 
             val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];