src/Pure/Syntax/syn_ext.ML

   val delims_of: xprod list -> string list list
   datatype syn_ext =
     Syn_Ext of {
       xprods: xprod list,
       consts: string list,
-      prmodes: string list,
       parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
       parse_rules: (Ast.ast * Ast.ast) list,
       parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
       print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
       print_rules: (Ast.ast * Ast.ast) list,
-      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
-      token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list}
+      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}
   val mfix_delims: string -> string list
   val mfix_args: string -> int
   val syn_ext': bool -> (string -> bool) -> mfix list ->
     string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
-    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
-    -> (string * string * (Proof.context -> string -> Pretty.T)) list
-    -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
+    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
+    (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext: mfix list -> string list ->
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
-    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
-    -> (string * string * (Proof.context -> string -> Pretty.T)) list
-    -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
+    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
+    (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext_const_names: string list -> syn_ext
   val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext_trfuns:
     (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((term list -> term) * stamp)) list *

   val syn_ext_advanced_trfuns:
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
-  val syn_ext_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> syn_ext
   val pure_ext: syn_ext
 end;
 
 structure Syn_Ext: SYN_EXT =
 struct

 
 datatype syn_ext =
   Syn_Ext of {
     xprods: xprod list,
     consts: string list,
-    prmodes: string list,
     parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
     parse_rules: (Ast.ast * Ast.ast) list,
     parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
     print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
     print_rules: (Ast.ast * Ast.ast) list,
-    print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
-    token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list};
+    print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list};
 
 
 (* syn_ext *)
 
-fun syn_ext' convert is_logtype mfixes consts trfuns tokentrfuns (parse_rules, print_rules) =
+fun syn_ext' convert is_logtype mfixes consts trfuns (parse_rules, print_rules) =
   let
     val (parse_ast_translation, parse_translation, print_translation,
       print_ast_translation) = trfuns;
 
     val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes

       distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
   in
     Syn_Ext {
       xprods = xprods,
       consts = union (op =) consts mfix_consts,
-      prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
       parse_ast_translation = parse_ast_translation,
       parse_rules = parse_rules' @ parse_rules,
       parse_translation = parse_translation,
       print_translation = print_translation,
       print_rules = map swap parse_rules' @ print_rules,
-      print_ast_translation = print_ast_translation,
-      token_translation = tokentrfuns}
+      print_ast_translation = print_ast_translation}
   end;
 
 
 val syn_ext = syn_ext' true (K false);
 
-fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) [] ([], []);
-fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) [] rules;
-fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
-fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []);
+fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []);
+fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
+fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []);
 
 fun syn_ext_trfuns (atrs, trs, tr's, atr's) =
   let fun simple (name, (f, s)) = (name, (K f, s)) in
     syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's)
   end;

    Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
    Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
    Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
   token_markers
   ([], [], [], [])
-  []
   ([], []);
 
 end;