src/HOL/Tools/Function/fun.ML

--- a/src/HOL/Tools/Function/fun.ML	Fri Mar 06 21:14:27 2015 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Fri Mar 06 21:20:30 2015 +0100
@@ -28,7 +28,6 @@
     fun err str = error (cat_lines ["Malformed definition:",
       str ^ " not allowed in sequential mode.",
       Syntax.string_of_term ctxt geq])
-    val thy = Proof_Context.theory_of ctxt
 
     fun check_constr_pattern (Bound _) = ()
       | check_constr_pattern t =