# HG changeset patch
# User wenzelm
# Date 1635182589 -7200
# Node ID bf703bfc065c43a6f2dd7669ae8f844908920b66
# Parent  9bfbb5f7ec99ea9645c6e309457f94c5ac37a0d2
clarified errors;

diff -r 9bfbb5f7ec99 -r bf703bfc065c src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Mon Oct 25 17:40:49 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Mon Oct 25 19:23:09 2021 +0200
@@ -13,9 +13,9 @@
   type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list
   type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   val instantiate_typ: insts -> typ -> typ
-  val instantiate_ctyp: cinsts -> ctyp -> ctyp
+  val instantiate_ctyp: Position.T -> cinsts -> ctyp -> ctyp
   val instantiate_term: insts -> term -> term
-  val instantiate_cterm: cinsts -> cterm -> cterm
+  val instantiate_cterm: Position.T -> cinsts -> cterm -> cterm
 end;
 
 structure ML_Antiquotations: ML_ANTIQUOTATIONS =
@@ -235,8 +235,12 @@
 type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list
 type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
 
-fun instantiate_typ (insts: insts) = Term_Subst.instantiateT (TVars.make (#1 insts));
-fun instantiate_ctyp (cinsts: cinsts) = Thm.instantiate_ctyp (TVars.make (#1 cinsts));
+fun instantiate_typ (insts: insts) =
+  Term_Subst.instantiateT (TVars.make (#1 insts));
+
+fun instantiate_ctyp pos (cinsts: cinsts) cT =
+  Thm.instantiate_ctyp (TVars.make (#1 cinsts)) cT
+  handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args));
 
 fun instantiate_term (insts: insts) =
   let
@@ -245,12 +249,13 @@
     val inst = Vars.make ((map o apfst o apsnd) instantiateT (#2 insts));
   in Term_Subst.instantiate_beta (instT, inst) end;
 
-fun instantiate_cterm (cinsts: cinsts) =
+fun instantiate_cterm pos (cinsts: cinsts) ct =
   let
     val cinstT = TVars.make (#1 cinsts);
     val instantiateT = Term_Subst.instantiateT (TVars.map (K Thm.typ_of) cinstT);
     val cinst = Vars.make ((map o apfst o apsnd) instantiateT (#2 cinsts));
-  in Thm.instantiate_beta_cterm (cinstT, cinst) end;
+  in Thm.instantiate_beta_cterm (cinstT, cinst) ct end
+  handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args));
 
 
 local
@@ -338,19 +343,25 @@
     val (ml_insts, t') = prepare_insts ctxt1 ctxt insts t;
   in prepare_ml range arg (ML_Syntax.print_term t') ml_insts ctxt end;
 
-fun typ_ml kind = (kind, "", "ML_Antiquotations.instantiate_typ");
-fun term_ml kind = (kind, "", "ML_Antiquotations.instantiate_term");
-fun ctyp_ml kind =
-  (kind, "ML_Antiquotations.make_ctyp ML_context", "ML_Antiquotations.instantiate_ctyp");
-fun cterm_ml kind =
-  (kind, "ML_Antiquotations.make_cterm ML_context", "ML_Antiquotations.instantiate_cterm");
+val ml_here = ML_Syntax.atomic o ML_Syntax.print_position;
+
+fun typ_ml (kind, _: Position.T) = (kind, "", "ML_Antiquotations.instantiate_typ ");
+fun term_ml (kind, _: Position.T) = (kind, "", "ML_Antiquotations.instantiate_term ");
+fun ctyp_ml (kind, pos) =
+  (kind, "ML_Antiquotations.make_ctyp ML_context",
+    "ML_Antiquotations.instantiate_ctyp " ^ ml_here pos);
+fun cterm_ml (kind, pos) =
+  (kind, "ML_Antiquotations.make_cterm ML_context",
+    "ML_Antiquotations.instantiate_cterm " ^ ml_here pos);
+
+val command_name = Parse.position o Parse.command_name;
 
 fun parse_body range =
-  (Parse.command_name "typ" >> typ_ml || Parse.command_name "ctyp" >> ctyp_ml) --
+  (command_name "typ" >> typ_ml || command_name "ctyp" >> ctyp_ml) --
     Parse.!!! Parse.typ >> prepare_type range ||
-  (Parse.command_name "term" >> term_ml || Parse.command_name "cterm" >> cterm_ml)
+  (command_name "term" >> term_ml || command_name "cterm" >> cterm_ml)
     -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_term range ||
-  (Parse.command_name "prop" >> term_ml || Parse.command_name "cprop" >> cterm_ml)
+  (command_name "prop" >> term_ml || command_name "cprop" >> cterm_ml)
     -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_prop range;
 
 val _ = Theory.setup