src/Pure/Syntax/syntax_phases.ML

           in [Ast.Constant (Lexicon.mark_class c)] end
       | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
           let
             val pos = Lexicon.pos_of_token tok;
             val (Type (c, _), rs) =
-              Proof_Context.check_type_name ctxt {proper = true, strict = false}
+              Proof_Context.check_type_name {proper = true, strict = false} ctxt
                 (Lexicon.str_of_token tok, pos);
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
       | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok

 (* decode_term -- transform parse tree into raw term *)
 
 fun decode_const ctxt (c, ps) =
   let
     val (Const (c', _), reports) =
-      Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
+      Proof_Context.check_const {proper = true, strict = false} ctxt (c, ps);
   in (c', reports) end;
 
 local
 
 fun get_free ctxt x =