# HG changeset patch
# User wenzelm
# Date 1374182024 -7200
# Node ID b824497c8e8670f4a77b1cfc9a93e259033b71ed
# Parent  d68fd63bf082f24cbadd55beff828906823c69a6
modify background theory where it is actually required (cf. 51dfdcd88e84);

diff -r d68fd63bf082 -r b824497c8e86 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:32:00 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Thu Jul 18 23:13:44 2013 +0200
@@ -313,11 +313,18 @@
 
 fun filter_solves ctxt goal =
   let
+    val thy' =
+      Proof_Context.theory_of ctxt
+      |> Context_Position.set_visible_global (Context_Position.is_visible ctxt)
+      |> Theory.checkpoint;
+    val ctxt' = Proof_Context.transfer thy' ctxt;
+    val goal' = Thm.transfer thy' goal;
+
     fun etacn thm i =
       Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
     fun try_thm thm =
-      if Thm.no_prems thm then rtac thm 1 goal
-      else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
+      if Thm.no_prems thm then rtac thm 1 goal'
+      else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
   in
     fn Internal (_, thm) =>
         if is_some (Seq.pull (try_thm thm))
@@ -625,18 +632,8 @@
         Toplevel.keep (fn state =>
           let
             val ctxt = Toplevel.context_of state;
-            val thy' =
-              Proof_Context.theory_of ctxt
-              |> Theory.copy
-              |> Context_Position.set_visible_global (Context_Position.is_visible ctxt)
-              |> Theory.checkpoint;
-
             val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
-            val (ctxt', opt_goal') =
-              (case opt_goal of
-                NONE => (ctxt, NONE)
-              | SOME th => (Proof_Context.transfer thy' ctxt, SOME (Thm.transfer thy' th)));
-          in print_theorems ctxt' opt_goal' opt_lim rem_dups spec end)));
+          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
 
 end;