src/Pure/Tools/find_theorems.ML
changeset 52788 da1fdbfebd39
parent 52704 b824497c8e86
child 52851 e71b5160f242
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Jul 30 12:07:14 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Jul 30 15:09:25 2013 +0200
     1.3 @@ -315,8 +315,7 @@
     1.4    let
     1.5      val thy' =
     1.6        Proof_Context.theory_of ctxt
     1.7 -      |> Context_Position.set_visible_global (Context_Position.is_visible ctxt)
     1.8 -      |> Theory.checkpoint;
     1.9 +      |> Context_Position.set_visible_global (Context_Position.is_visible ctxt);
    1.10      val ctxt' = Proof_Context.transfer thy' ctxt;
    1.11      val goal' = Thm.transfer thy' goal;
    1.12