src/Pure/Isar/proof_context.ML

   val get_case: Proof.context -> string -> string option list -> RuleCases.T
   val add_notation: Syntax.mode -> (term * mixfix) list ->
     Proof.context -> Proof.context
   val target_notation: Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
-  val set_expand_abbrevs: bool -> Proof.context -> Proof.context
   val add_abbrev: string -> bstring * term -> Proof.context -> (term * term) * Proof.context
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit

 
 (** Isar proof context information **)
 
 datatype ctxt =
   Ctxt of
-   {mode: mode,                                   (*inner syntax mode*)
-    naming: NameSpace.naming,                     (*local naming conventions*)
-    syntax: LocalSyntax.T,                        (*local syntax*)
-    consts: Consts.T * Consts.T,                  (*global/local consts*)
-    thms: thm list NameSpace.table * FactIndex.T, (*local thms*)
-    cases: (string * (RuleCases.T * bool)) list}; (*local contexts*)
+   {mode: mode,                                       (*inner syntax mode*)
+    naming: NameSpace.naming,                         (*local naming conventions*)
+    syntax: LocalSyntax.T,                            (*local syntax*)
+    consts: Consts.T * Consts.T,                      (*global/local consts*)
+    thms: thm list NameSpace.table * FactIndex.T,     (*local thms*)
+    cases: (string * (RuleCases.T * bool)) list};     (*local contexts*)
 
 fun make_ctxt (mode, naming, syntax, consts, thms, cases) =
   Ctxt {mode = mode, naming = naming, syntax = syntax,
     consts = consts, thms = thms, cases = cases};
 

 
 (** pretty printing **)
 
 local
 
-fun rewrite_term warn thy rews t =
-  if can Term.type_of t then Pattern.rewrite_term thy rews [] t
-  else (if warn then warning "Printing malformed term -- cannot expand abbreviations" else (); t);
+fun rewrite_term thy rews t =
+  if can Term.type_of t then Pattern.rewrite_term thy rews [] t else t;
 
 fun pretty_term' abbrevs ctxt t =
   let
     val thy = theory_of ctxt;
     val syntax = syntax_of ctxt;
     val consts = consts_of ctxt;
     val do_abbrevs = abbrevs andalso not (print_mode_active "no_abbrevs");
     val t' = t
-      |> do_abbrevs ? rewrite_term true thy (Consts.abbrevs_of consts (print_mode_value () @ [""]))
-      |> do_abbrevs ? rewrite_term false thy (Consts.abbrevs_of consts [Syntax.internalM])
+      |> do_abbrevs ? rewrite_term thy (Consts.abbrevs_of consts (print_mode_value () @ [""]))
+      |> do_abbrevs ? rewrite_term thy (Consts.abbrevs_of consts [Syntax.internalM])
       |> Sign.extern_term (Consts.extern_early consts) thy
       |> LocalSyntax.extern_term syntax;
   in Sign.pretty_term' ctxt (LocalSyntax.syn_of syntax) (Consts.extern consts) t' end;
 
 in

 (* local abbreviations *)
 
 local
 
 fun certify_consts ctxt =
-  Consts.certify (pp ctxt) (tsig_of ctxt) (consts_of ctxt);
+  let val Mode {abbrev, ...} = get_mode ctxt
+  in Consts.certify (pp ctxt) (tsig_of ctxt) (not abbrev) (consts_of ctxt) end;
 
 fun reject_schematic (Var (xi, _)) =
       error ("Unbound schematic variable: " ^ Term.string_of_vname xi)
   | reject_schematic (Abs (_, _, t)) = reject_schematic t
   | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)

 
 fun gen_cert prop mode ctxt0 t =
   let val ctxt = set_mode mode ctxt0 in
     t
     |> expand_abbrevs ctxt
-    |> (fn t' => #1 (Sign.certify' false prop (pp ctxt) (consts_of ctxt) (theory_of ctxt) t')
+    |> (fn t' => #1 (Sign.certify' prop (pp ctxt) false (consts_of ctxt) (theory_of ctxt) t')
       handle TYPE (msg, _, _) => error msg
         | TERM (msg, _) => error msg)
    end;
 
 in

 
 local
 
 fun gen_bind prep (xi as (x, _), raw_t) ctxt =
   ctxt
-  |> set_mode mode_default
-  |> Variable.add_binds [(xi, Option.map (prep ctxt) raw_t)];
+  |> Variable.add_binds [(xi, Option.map (prep (set_mode mode_default ctxt)) raw_t)];
 
 in
 
 fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
   | drop_schematic b = b;

   in Context.mapping (Sign.add_notation mode args') (add_notation mode args') end;
 
 
 (* abbreviations *)
 
-val set_expand_abbrevs = map_consts o apsnd o Consts.set_expand;
-fun read_term_abbrev ctxt = Syntax.read_term (set_expand_abbrevs false ctxt);
+fun read_term_abbrev ctxt = Syntax.read_term (set_mode mode_abbrev ctxt);
 
 fun add_abbrev mode (c, raw_t) ctxt =
   let
-    val t0 = cert_term (ctxt |> set_expand_abbrevs false) raw_t
+    val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val ((lhs, rhs), consts') = consts_of ctxt
       |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode (c, t);
   in