src/Pure/Syntax/syntax_ext.ML

--- a/src/Pure/Syntax/syntax_ext.ML	Thu Jan 03 16:53:18 2019 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Thu Jan 03 20:16:42 2019 +0100
@@ -33,18 +33,12 @@
   val mfix_args: Symbol_Pos.T list -> int
   val mixfix_args: Input.source -> int
   val escape: string -> string
-  val syn_ext': string list -> mfix list ->
+  val syn_ext: string list -> mfix list ->
     (string * 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 ->
     (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
-  val syn_ext: mfix list -> (string * 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 ->
-    (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext_trfuns:
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
@@ -406,7 +400,7 @@
 
 (* syn_ext *)
 
-fun syn_ext' logical_types mfixes consts trfuns (parse_rules, print_rules) =
+fun syn_ext logical_types mfixes consts trfuns (parse_rules, print_rules) =
   let
     val (parse_ast_translation, parse_translation, print_translation,
       print_ast_translation) = trfuns;
@@ -429,10 +423,8 @@
   end;
 
 
-val syn_ext = syn_ext' [];
-
-fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
-fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns ([], []);
+fun syn_ext_rules rules = syn_ext [] [] [] ([], [], [], []) rules;
+fun syn_ext_trfuns trfuns = syn_ext [] [] [] trfuns ([], []);
 
 fun stamp_trfun s (c, f) = (c, (f, s));
 fun mk_trfun tr = stamp_trfun (stamp ()) tr;