src/Pure/Proof/proof_syntax.ML

   val proofT: typ
   val add_proof_syntax: theory -> theory
   val proof_of_term: theory -> bool -> term -> Proofterm.proof
   val term_of_proof: Proofterm.proof -> term
   val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
-  val strip_sorts_consttypes: Proof.context -> Proof.context
   val read_term: theory -> bool -> typ -> string -> term
   val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
   val proof_syntax: Proofterm.proof -> theory -> theory
   val proof_of: bool -> thm -> Proofterm.proof
   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T

         (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);
   in
     (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
   end;
 
-fun strip_sorts_consttypes ctxt =
-  let val {constants = (_, tab), ...} = Consts.dest (Proof_Context.consts_of ctxt)
-  in Symtab.fold (fn (s, (T, _)) =>
-      Proof_Context.add_const_constraint (s, SOME (Type.strip_sorts T)))
-    tab ctxt
-  end;
-
 fun read_term thy topsort =
   let
     val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy));
     val axm_names = map fst (Theory.all_axioms_of thy);
     val ctxt = thy

       |> add_proof_atom_consts
         (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
       |> Proof_Context.init_global
       |> Proof_Context.allow_dummies
       |> Proof_Context.set_mode Proof_Context.mode_schematic
-      |> (if topsort then
-            strip_sorts_consttypes #>
-            Proof_Context.set_defsort []
-          else I);
+      |> topsort ? (Config.put Type_Infer_Context.const_sorts false #> Proof_Context.set_defsort []);
   in
     fn ty => fn s =>
       (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
       |> Type.constraint ty |> Syntax.check_term ctxt
   end;