# HG changeset patch
# User haftmann
# Date 1208845993 -7200
# Node ID 48df747c8543ee54310fa5981de5de11f436af3d
# Parent  bbb5e6904d7857a44dc7ade2e09432d0f129f3b0
exported is_abbrev mode discriminator

diff -r bbb5e6904d78 -r 48df747c8543 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Apr 22 08:33:12 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 22 08:33:13 2008 +0200
@@ -20,6 +20,7 @@
   val set_mode: mode -> Proof.context -> Proof.context
   val get_mode: Proof.context -> mode
   val restore_mode: Proof.context -> Proof.context -> Proof.context
+  val is_abbrev_mode: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
   val naming_of: Proof.context -> NameSpace.naming
   val full_name: Proof.context -> bstring -> string
@@ -165,6 +166,8 @@
 fun make_mode (stmt, pattern, schematic, abbrev) =
   Mode {stmt = stmt, pattern = pattern, schematic = schematic, abbrev = abbrev};
 
+fun dest_mode (Mode mode) = mode;
+
 val mode_default   = make_mode (false, false, false, false);
 val mode_stmt      = make_mode (true, false, false, false);
 val mode_pattern   = make_mode (false, true, false, false);
@@ -444,11 +447,12 @@
 
 val tsig_of = Sign.tsig_of o ProofContext.theory_of;
 
+val is_abbrev_mode = #abbrev o dest_mode o get_mode;
+
 local
 
-fun certify_consts ctxt =
-  let val Mode {abbrev, ...} = get_mode ctxt
-  in Consts.certify (Syntax.pp ctxt) (tsig_of ctxt) (not abbrev) (consts_of ctxt) end;
+fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
+  (not (is_abbrev_mode ctxt)) (consts_of ctxt);
 
 fun reject_schematic (Var (xi, _)) =
       error ("Unbound schematic variable: " ^ Term.string_of_vname xi)