# HG changeset patch
# User wenzelm
# Date 1228988497 -3600
# Node ID d219318fd89a6484adf11886bab6f419bf45db72
# Parent  dc08e3990c77590488b1f7cc00bc890560de17df
Theory.checkpoint before commencing proof;

diff -r dc08e3990c77 -r d219318fd89a src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Thu Dec 11 00:42:52 2008 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Thu Dec 11 10:41:37 2008 +0100
@@ -108,6 +108,7 @@
         thy
         |> Sign.add_consts_i [(name, setT', NoSyn)]
         |> PureThy.add_defs false [Thm.no_attributes (PrimitiveDefs.mk_defpair (setC, set))]
+        ||> Theory.checkpoint
         |-> (fn [th] => pair (SOME th))
       else (NONE, thy);