# HG changeset patch
# User blanchet
# Date 1292510672 -3600
# Node ID 15fbf30288e1b631fb75fe7584cc4e3400d188ef
# Parent  91fab0d3553b2b5261aecf1703f06e2cab3aeefa
removed unused variable

diff -r 91fab0d3553b -r 15fbf30288e1 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 16 15:44:32 2010 +0100
@@ -536,7 +536,6 @@
       val reconstructor = Unsynchronized.ref ""
       val named_thms =
         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
-      val ctxt = Proof.context_of pre
       val minimize = AList.defined (op =) args minimizeK
       val metis_ft = AList.defined (op =) args metis_ftK
       val trivial =