src/Pure/Tools/find_theorems.ML
changeset 52701 51dfdcd88e84
parent 51717 9e7d1c139569
child 52702 c503730efae5
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Jul 18 21:57:27 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:00:35 2013 +0200
     1.3 @@ -631,8 +631,18 @@
     1.4          Toplevel.keep (fn state =>
     1.5            let
     1.6              val ctxt = Toplevel.context_of state;
     1.7 +            val thy' =
     1.8 +              Proof_Context.theory_of ctxt
     1.9 +              |> Theory.copy
    1.10 +              |> Context_Position.set_visible_global (Context_Position.is_visible ctxt)
    1.11 +              |> Theory.checkpoint;
    1.12 +
    1.13              val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
    1.14 -          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
    1.15 +            val (ctxt', opt_goal') =
    1.16 +              (case opt_goal of
    1.17 +                NONE => (ctxt, NONE)
    1.18 +              | SOME th => (Proof_Context.transfer thy' ctxt, SOME (Thm.transfer thy' th)));
    1.19 +          in print_theorems ctxt' opt_goal' opt_lim rem_dups spec end)));
    1.20  
    1.21  end;
    1.22