# HG changeset patch
# User wenzelm
# Date 1222089971 -7200
# Node ID 83c4fc3834090defa91fc83253fb8f5d41ae614c
# Parent  b17d863a050f2a327f37f2e3c6153f073cf3dcf9
added reject_draft;

diff -r b17d863a050f -r 83c4fc383409 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Sep 22 15:26:07 2008 +0200
+++ b/src/Pure/context.ML	Mon Sep 22 15:26:11 2008 +0200
@@ -24,6 +24,7 @@
   val is_stale: theory -> bool
   val PureN: string
   val is_draft: theory -> bool
+  val reject_draft: theory -> theory
   val exists_name: string -> theory -> bool
   val names_of: theory -> string list
   val pretty_thy: theory -> Pretty.T
@@ -202,6 +203,10 @@
 fun draft_id (_, name) = (name = draftN);
 val is_draft = draft_id o #id o identity_of;
 
+fun reject_draft thy =
+  if is_draft thy then raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy])
+  else thy;
+
 fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) =
   name = theory_name thy orelse
   name = #2 id orelse