# HG changeset patch
# User wenzelm
# Date 1635184332 -7200
# Node ID d114553793df70af1c2bf51ebe4d10a5dbcaf9df
# Parent  bf703bfc065c43a6f2dd7669ae8f844908920b66
tuned comments;

diff -r bf703bfc065c -r d114553793df src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Mon Oct 25 19:23:09 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Mon Oct 25 19:52:12 2021 +0200
@@ -227,7 +227,7 @@
    (Scan.succeed "ML_Antiquotations.dest_judgment ML_context"));
 
 
-(* type/term instantiations and constructors *)
+(* type/term instantiations *)
 
 fun make_ctyp ctxt T = Thm.ctyp_of ctxt T |> Thm.trim_context_ctyp;
 fun make_cterm ctxt t = Thm.cterm_of ctxt t |> Thm.trim_context_cterm;
@@ -384,6 +384,8 @@
 in end;
 
 
+(* type/term constructors *)
+
 local
 
 val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords;