src/Pure/ML/ml_antiquote.ML

 (* type constructors *)
 
 fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
-      val Type (c, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s;
+      val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
       val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
       val res =
         (case try check (c, decl) of
           SOME res => res
         | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));

 (* constants *)
 
 fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
-      val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} s;
+      val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
       val res = check (Proof_Context.consts_of ctxt, c)
         handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
     in ML_Syntax.print_string res end);
 
 val _ = Theory.setup

     (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
         (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
       >> (fn ((ctxt, raw_c), Ts) =>
         let
           val Const (c, _) =
-            Proof_Context.read_const ctxt {proper = true, strict = true} raw_c;
+            Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
           val consts = Proof_Context.consts_of ctxt;
           val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
           val _ = length Ts <> n andalso
             error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
               quote c ^ enclose "(" ")" (commas (replicate n "_")));