src/Pure/context.ML
changeset 28317 83c4fc383409
parent 28122 3d099ce624e7
child 28375 c879d88d038a
--- 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