# HG changeset patch
# User haftmann
# Date 1250342994 -7200
# Node ID a97e9caebd60ae95fb749ffda721a562856fa9ba
# Parent  89b19ab3b35c08731f7c46c2d7d55669f23adde6
additional checkpoints avoid problems in error situations

diff -r 89b19ab3b35c -r a97e9caebd60 src/Pure/Isar/class_target.ML
--- 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
diff -r 89b19ab3b35c -r a97e9caebd60 src/Pure/Isar/overloading.ML
--- 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