# HG changeset patch
# User wenzelm
# Date 1635103195 -7200
# Node ID d3e36521fcc77efc33609e5b97805efc51cf1f6e
# Parent  7625b5d7cfe2cd7dfa848ef3a624497127a50529
more markup;

diff -r 7625b5d7cfe2 -r d3e36521fcc7 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sun Oct 24 20:25:51 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Sun Oct 24 21:19:55 2021 +0200
@@ -279,9 +279,10 @@
     SOME S => (a, S)
   | NONE => error ("No occurrence of type variable " ^ quote a ^ Position.here pos));
 
-fun get_free env (x, pos) =
+fun check_free ctxt env (x, pos) =
   (case AList.lookup (op =) env x of
-    SOME T => (x, T)
+    SOME T =>
+      (Context_Position.reports ctxt (map (pair pos) (Syntax_Phases.markup_free ctxt x)); (x, T))
   | NONE => error ("No occurrence of variable " ^ quote x ^ Position.here pos));
 
 fun make_instT (a, pos) T =
@@ -299,7 +300,7 @@
     val envT = Term.add_tfrees t [];
     val env = Term.add_frees t [];
     val freesT = map (Logic.mk_type o TFree o get_tfree envT) instT;
-    val frees = map (Free o get_free env) inst;
+    val frees = map (Free o check_free ctxt1 env) inst;
     val (t' :: varsT, vars) =
       Variable.export_terms ctxt1 ctxt0 (t :: freesT @ frees)
       |> chop (1 + length freesT);
diff -r 7625b5d7cfe2 -r d3e36521fcc7 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Oct 24 20:25:51 2021 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Oct 24 21:19:55 2021 +0200
@@ -7,6 +7,7 @@
 
 signature SYNTAX_PHASES =
 sig
+  val markup_free: Proof.context -> string -> Markup.T list
   val reports_of_scope: Position.T list -> Position.report list
   val decode_sort: term -> sort
   val decode_typ: term -> typ