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