src/Pure/Isar/proof_context.ML

     val t' = t
       |> do_abbrevs ? rewrite_term true thy (Consts.abbrevs_of consts (! print_mode @ [""]))
       |> do_abbrevs ? rewrite_term false thy (Consts.abbrevs_of consts [#1 Syntax.internal_mode])
       |> Sign.extern_term (Consts.extern_early consts) thy
       |> LocalSyntax.extern_term syntax;
-  in
-    Sign.pretty_term' (Context.Proof ctxt) (LocalSyntax.syn_of syntax) (Consts.extern consts) t'
-  end;
+  in Sign.pretty_term' ctxt (LocalSyntax.syn_of syntax) (Consts.extern consts) t' end;
 
 in
 
 val pretty_term = pretty_term' true;
 val pretty_term_abbrev = pretty_term' false;

 (** prepare types **)
 
 local
 
 fun read_typ_aux read ctxt s =
-  read (syn_of ctxt) (Context.Proof ctxt) (Variable.def_sort ctxt) s;
+  read (syn_of ctxt) ctxt (Variable.def_sort ctxt) s;
 
 fun cert_typ_aux cert ctxt raw_T =
   cert (theory_of ctxt) raw_T handle TYPE (msg, _, _) => error msg;
 
 in

 
 (* read wrt. theory *)     (*exception ERROR*)
 
 fun read_def_termTs freeze pp syn ctxt (types, sorts, used) sTs =
   Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn (consts_of ctxt)
-    (Context.Proof ctxt) (types, sorts) used freeze sTs;
+    ctxt (types, sorts) used freeze sTs;
 
 fun read_def_termT freeze pp syn ctxt defaults sT =
   apfst hd (read_def_termTs freeze pp syn ctxt defaults [sT]);
 
 fun read_term_thy freeze pp syn thy defaults s =

 fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx))
   | const_syntax ctxt (Const (c, _), mx) =
       Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
   | const_syntax _ _ = NONE;
 
-fun context_const_ast_tr context [Syntax.Variable c] =
+fun context_const_ast_tr ctxt [Syntax.Variable c] =
       let
-        val consts = Context.cases Sign.consts_of consts_of context;
+        val consts = consts_of ctxt;
         val c' = Consts.intern consts c;
         val _ = Consts.the_constraint consts c' handle TYPE (msg, _, _) => error msg;
       in Syntax.Constant (Syntax.constN ^ c') end
   | context_const_ast_tr _ asts = raise Syntax.AST ("const_ast_tr", asts);