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