--- 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;
--- 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;