author wenzelm Thu, 18 Jul 2013 23:13:44 +0200 changeset 52704 b824497c8e86 parent 52703 d68fd63bf082 child 52705 c12602c1b13b
modify background theory where it is actually required (cf. 51dfdcd88e84);
```--- 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;
```