# HG changeset patch
# User wenzelm
# Date 1730055449 -3600
# Node ID d2e39f0f9b40f2cb4505350b6e1f762e71035459
# Parent  41e843d901ee4ae8415ecdf76f953476cd349e3d
markup for "..." notation;
clarified signature;

diff -r 41e843d901ee -r d2e39f0f9b40 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Sun Oct 27 15:30:00 2024 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Sun Oct 27 19:57:29 2024 +0100
@@ -12,7 +12,9 @@
   val assmsN: string
   val abs_params: term -> term -> term
   val goal: Proof.context -> term list -> (indexname * term option) list
-  val dddot: indexname
+  val dddot_name: string
+  val dddot_indexname: indexname
+  val dddot_vname: string
   val facts: Proof.context -> term list -> (indexname * term option) list
   val no_facts: indexname list
 end;
@@ -43,11 +45,9 @@
 
 (* dddot *)
 
-val dddot = ("dddot", 0);
-
-val _ =
-  Theory.setup (Sign.parse_translation
-    [("_DDDOT", fn _ => fn ts => Term.list_comb (Syntax.var dddot, ts))]);
+val dddot_name = "dddot";
+val dddot_indexname = (dddot_name, 0);
+val dddot_vname = Term.string_of_vname dddot_indexname;
 
 
 (* facts *)
@@ -60,8 +60,8 @@
 fun facts ctxt props =
   (case try List.last props of
     NONE => []
-  | SOME prop => [(dddot, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
+  | SOME prop => [(dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
 
-val no_facts = [dddot, (thisN, 0)];
+val no_facts = [dddot_indexname, (thisN, 0)];
 
 end;
diff -r 41e843d901ee -r d2e39f0f9b40 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Oct 27 15:30:00 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Oct 27 19:57:29 2024 +0100
@@ -202,6 +202,8 @@
               |>> dest_Type_name;
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_type c)] end
+      | asts_of (Parser.Node ({const = "_DDDOT", ...}, [Parser.Tip tok])) =
+          [Ast.constrain (Ast.Variable Auto_Bind.dddot_vname) (ast_of_position tok)]
       | asts_of (Parser.Node ({const = "_position", ...}, [Parser.Tip tok])) =
           asts_of_position "_constrain" tok
       | asts_of (Parser.Node ({const = "_position_sort", ...}, [Parser.Tip tok])) =
@@ -662,7 +664,7 @@
             else Syntax.const "_free" $ t
           end
       | mark (t as Var (xi, T)) =
-          if xi = Auto_Bind.dddot then Const ("_DDDOT", T)
+          if xi = Auto_Bind.dddot_indexname then Const ("_DDDOT", T)
           else Syntax.const "_var" $ t
       | mark a = a;
   in mark tm end;