src/Pure/context.ML
changeset 28317 83c4fc383409
parent 28122 3d099ce624e7
child 28375 c879d88d038a
     1.1 --- a/src/Pure/context.ML	Mon Sep 22 15:26:07 2008 +0200
     1.2 +++ b/src/Pure/context.ML	Mon Sep 22 15:26:11 2008 +0200
     1.3 @@ -24,6 +24,7 @@
     1.4    val is_stale: theory -> bool
     1.5    val PureN: string
     1.6    val is_draft: theory -> bool
     1.7 +  val reject_draft: theory -> theory
     1.8    val exists_name: string -> theory -> bool
     1.9    val names_of: theory -> string list
    1.10    val pretty_thy: theory -> Pretty.T
    1.11 @@ -202,6 +203,10 @@
    1.12  fun draft_id (_, name) = (name = draftN);
    1.13  val is_draft = draft_id o #id o identity_of;
    1.14  
    1.15 +fun reject_draft thy =
    1.16 +  if is_draft thy then raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy])
    1.17 +  else thy;
    1.18 +
    1.19  fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) =
    1.20    name = theory_name thy orelse
    1.21    name = #2 id orelse