# HG changeset patch
# User wenzelm
# Date 1459350206 -7200
# Node ID 3e9a68bd30a77b1d969d5963960b959dc2080f47
# Parent  ac039c4981b6ff5ccb06d7fbc52a7206dcd0f918
clarified modules;

diff -r ac039c4981b6 -r 3e9a68bd30a7 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Wed Mar 30 16:36:23 2016 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Wed Mar 30 17:03:26 2016 +0200
@@ -12,6 +12,7 @@
   val assmsN: string
   val abs_params: term -> term -> term
   val goal: Proof.context -> term list -> (indexname * term option) list
+  val dddot: indexname
   val facts: Proof.context -> term list -> (indexname * term option) list
   val no_facts: indexname list
 end;
@@ -40,6 +41,15 @@
   | goal _ _ = [((thesisN, 0), NONE)];
 
 
+(* dddot *)
+
+val dddot = ("dddot", 0);
+
+val _ =
+  Theory.setup (Sign.parse_translation
+    [("_DDDOT", fn _ => fn ts => Term.list_comb (Syntax.var dddot, ts))]);
+
+
 (* facts *)
 
 fun get_arg ctxt prop =
@@ -50,9 +60,8 @@
 fun facts ctxt props =
   (case try List.last props of
     NONE => []
-  | SOME prop =>
-      [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
+  | SOME prop => [(dddot, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
 
-val no_facts = [Syntax_Ext.dddot_indexname, (thisN, 0)];
+val no_facts = [dddot, (thisN, 0)];
 
 end;
diff -r ac039c4981b6 -r 3e9a68bd30a7 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Wed Mar 30 16:36:23 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Wed Mar 30 17:03:26 2016 +0200
@@ -6,7 +6,6 @@
 
 signature SYNTAX_EXT =
 sig
-  val dddot_indexname: indexname
   datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
   val typ_to_nonterm: typ -> string
   datatype xsymb =
@@ -56,12 +55,6 @@
 structure Syntax_Ext: SYNTAX_EXT =
 struct
 
-
-(** misc definitions **)
-
-val dddot_indexname = ("dddot", 0);
-
-
 (** datatype xprod **)
 
 (*Delim s: delimiter s
diff -r ac039c4981b6 -r 3e9a68bd30a7 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Mar 30 16:36:23 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Mar 30 17:03:26 2016 +0200
@@ -624,7 +624,7 @@
             else Syntax.const "_free" $ t
           end
       | mark (t as Var (xi, T)) =
-          if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
+          if xi = Auto_Bind.dddot then Const ("_DDDOT", T)
           else Syntax.const "_var" $ t
       | mark a = a;
   in mark tm end;
diff -r ac039c4981b6 -r 3e9a68bd30a7 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Wed Mar 30 16:36:23 2016 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Wed Mar 30 17:03:26 2016 +0200
@@ -184,11 +184,6 @@
   | type_tr ts = raise TERM ("type_tr", ts);
 
 
-(* dddot *)
-
-fun dddot_tr ts = Term.list_comb (Syntax.var Syntax_Ext.dddot_indexname, ts);
-
-
 (* quote / antiquote *)
 
 fun antiquote_tr name =
@@ -495,7 +490,6 @@
   ("_ofclass", fn _ => ofclass_tr),
   ("_sort_constraint", fn _ => sort_constraint_tr),
   ("_TYPE", fn _ => type_tr),
-  ("_DDDOT", fn _ => dddot_tr),
   ("_update_name", fn _ => update_name_tr),
   ("_index", fn _ => index_tr),
   ("_struct", struct_tr)];