exported is_abbrev mode discriminator
authorhaftmann
Tue Apr 22 08:33:13 2008 +0200 (2008-04-22 ago)
changeset 2673148df747c8543
parent 26730 bbb5e6904d78
child 26732 6ea9de67e576
exported is_abbrev mode discriminator
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Apr 22 08:33:12 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Apr 22 08:33:13 2008 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4    val set_mode: mode -> Proof.context -> Proof.context
     1.5    val get_mode: Proof.context -> mode
     1.6    val restore_mode: Proof.context -> Proof.context -> Proof.context
     1.7 +  val is_abbrev_mode: Proof.context -> bool
     1.8    val set_stmt: bool -> Proof.context -> Proof.context
     1.9    val naming_of: Proof.context -> NameSpace.naming
    1.10    val full_name: Proof.context -> bstring -> string
    1.11 @@ -165,6 +166,8 @@
    1.12  fun make_mode (stmt, pattern, schematic, abbrev) =
    1.13    Mode {stmt = stmt, pattern = pattern, schematic = schematic, abbrev = abbrev};
    1.14  
    1.15 +fun dest_mode (Mode mode) = mode;
    1.16 +
    1.17  val mode_default   = make_mode (false, false, false, false);
    1.18  val mode_stmt      = make_mode (true, false, false, false);
    1.19  val mode_pattern   = make_mode (false, true, false, false);
    1.20 @@ -444,11 +447,12 @@
    1.21  
    1.22  val tsig_of = Sign.tsig_of o ProofContext.theory_of;
    1.23  
    1.24 +val is_abbrev_mode = #abbrev o dest_mode o get_mode;
    1.25 +
    1.26  local
    1.27  
    1.28 -fun certify_consts ctxt =
    1.29 -  let val Mode {abbrev, ...} = get_mode ctxt
    1.30 -  in Consts.certify (Syntax.pp ctxt) (tsig_of ctxt) (not abbrev) (consts_of ctxt) end;
    1.31 +fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
    1.32 +  (not (is_abbrev_mode ctxt)) (consts_of ctxt);
    1.33  
    1.34  fun reject_schematic (Var (xi, _)) =
    1.35        error ("Unbound schematic variable: " ^ Term.string_of_vname xi)