src/HOL/Tools/Function/function_elims.ML

--- a/src/HOL/Tools/Function/function_elims.ML	Fri Mar 06 21:14:27 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML	Fri Mar 06 21:20:30 2015 +0100
@@ -79,8 +79,6 @@
 
 fun mk_partial_elim_rules ctxt result =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
     val n_fs = length fs;