additional checkpoints avoid problems in error situations

--- a/src/Pure/Isar/class_target.ML	Sat Aug 15 15:29:53 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Sat Aug 15 15:29:54 2009 +0200
@@ -513,6 +513,7 @@
       | NONE => NONE;
   in
     thy
+    |> Theory.checkpoint
     |> ProofContext.init
     |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
     |> fold (Variable.declare_typ o TFree) vs

--- a/src/Pure/Isar/overloading.ML	Sat Aug 15 15:29:53 2009 +0200
+++ b/src/Pure/Isar/overloading.ML	Sat Aug 15 15:29:54 2009 +0200
@@ -154,6 +154,7 @@
     val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
   in
     thy
+    |> Theory.checkpoint
     |> ProofContext.init
     |> OverloadingData.put overloading
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading