src/Pure/meta_simplifier.ML

--- a/src/Pure/meta_simplifier.ML	Mon Apr 26 16:08:04 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Apr 26 20:30:50 2010 +0200
@@ -834,7 +834,6 @@
   in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
   handle THM _ =>
     let
-      val thy = Thm.theory_of_thm thm;
       val _ $ _ $ prop0 = Thm.prop_of thm;
     in
       trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';