src/Pure/Syntax/syn_ext.ML

--- a/src/Pure/Syntax/syn_ext.ML	Thu Apr 07 17:52:44 2011 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Thu Apr 07 18:24:59 2011 +0200
@@ -41,30 +41,26 @@
     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:
@@ -77,7 +73,6 @@
     (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;
 
@@ -326,19 +321,17 @@
   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;
@@ -351,23 +344,20 @@
     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
@@ -394,7 +384,6 @@
    Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
   token_markers
   ([], [], [], [])
-  []
   ([], []);
 
 end;