# 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