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;