extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;

--- a/src/Pure/Isar/toplevel.ML	Wed Mar 27 19:32:44 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 27 20:57:05 2013 +0100
@@ -548,7 +548,7 @@
 
 fun theory_to_proof f = begin_proof
   (fn _ => fn gthy =>
-    (Context.Theory o Sign.reset_group o Proof_Context.theory_of,
+    (Context.Theory o Theory.checkpoint o Sign.reset_group o Proof_Context.theory_of,
       (case gthy of
         Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))
       | _ => raise UNDEF)));