src/Pure/Tools/find_theorems.ML
 changeset 52704 b824497c8e86 parent 52703 d68fd63bf082 child 52788 da1fdbfebd39
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:32:00 2013 +0200
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Jul 18 23:13:44 2013 +0200
1.3 @@ -313,11 +313,18 @@
1.4
1.5  fun filter_solves ctxt goal =
1.6    let
1.7 +    val thy' =
1.8 +      Proof_Context.theory_of ctxt
1.9 +      |> Context_Position.set_visible_global (Context_Position.is_visible ctxt)
1.10 +      |> Theory.checkpoint;
1.11 +    val ctxt' = Proof_Context.transfer thy' ctxt;
1.12 +    val goal' = Thm.transfer thy' goal;
1.13 +
1.14      fun etacn thm i =
1.15        Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
1.16      fun try_thm thm =
1.17 -      if Thm.no_prems thm then rtac thm 1 goal
1.18 -      else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
1.19 +      if Thm.no_prems thm then rtac thm 1 goal'
1.20 +      else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
1.21    in
1.22      fn Internal (_, thm) =>
1.23          if is_some (Seq.pull (try_thm thm))
1.24 @@ -625,18 +632,8 @@
1.25          Toplevel.keep (fn state =>
1.26            let
1.27              val ctxt = Toplevel.context_of state;
1.28 -            val thy' =
1.29 -              Proof_Context.theory_of ctxt
1.30 -              |> Theory.copy
1.31 -              |> Context_Position.set_visible_global (Context_Position.is_visible ctxt)
1.32 -              |> Theory.checkpoint;
1.33 -
1.34              val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
1.35 -            val (ctxt', opt_goal') =
1.36 -              (case opt_goal of
1.37 -                NONE => (ctxt, NONE)
1.38 -              | SOME th => (Proof_Context.transfer thy' ctxt, SOME (Thm.transfer thy' th)));
1.39 -          in print_theorems ctxt' opt_goal' opt_lim rem_dups spec end)));
1.40 +          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
1.41
1.42  end;
1.43
```