added is_draft;
authorwenzelm
Wed Feb 03 16:42:40 1999 +0100 (1999-02-03)
changeset 6188c40e5ac04e3e
parent 6187 c6c4626ef693
child 6189 e9dc9ec28a2d
added is_draft;
renamed sig to PRIVATE_THEORY;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Wed Feb 03 16:41:49 1999 +0100
     1.2 +++ b/src/Pure/theory.ML	Wed Feb 03 16:42:40 1999 +0100
     1.3 @@ -17,6 +17,7 @@
     1.4        parents: theory list,
     1.5        ancestors: theory list}
     1.6    val sign_of: theory -> Sign.sg
     1.7 +  val is_draft: theory -> bool
     1.8    val syn_of: theory -> Syntax.syntax
     1.9    val parents_of: theory -> theory list
    1.10    val ancestors_of: theory -> theory list
    1.11 @@ -84,7 +85,7 @@
    1.12    val pre_pure: theory
    1.13  end;
    1.14  
    1.15 -signature THEORY_PRIVATE =
    1.16 +signature PRIVATE_THEORY =
    1.17  sig
    1.18    include THEORY
    1.19    val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
    1.20 @@ -95,7 +96,7 @@
    1.21  end;
    1.22  
    1.23  
    1.24 -structure Theory: THEORY_PRIVATE =
    1.25 +structure Theory: PRIVATE_THEORY =
    1.26  struct
    1.27  
    1.28  
    1.29 @@ -116,6 +117,7 @@
    1.30  fun rep_theory (Theory args) = args;
    1.31  
    1.32  val sign_of = #sign o rep_theory;
    1.33 +val is_draft = Sign.is_draft o sign_of;
    1.34  val syn_of = #syn o Sign.rep_sg o sign_of;
    1.35  val parents_of = #parents o rep_theory;
    1.36  val ancestors_of = #ancestors o rep_theory;
    1.37 @@ -410,7 +412,7 @@
    1.38  fun prep_ext_merge thys =
    1.39    if null thys then
    1.40      error "Merge: no parent theories"
    1.41 -  else if exists (Sign.is_draft o sign_of) thys then
    1.42 +  else if exists is_draft thys then
    1.43      error "Attempt to merge draft theories"
    1.44    else
    1.45      let