--- 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;