# HG changeset patch
# User wenzelm
# Date 1546543002 -3600
# Node ID a91e32843310817a2e7e4bf0bbcbabb14dc33119
# Parent  b0568a9dd1607be13d723d5c1fa01925a8606973
tuned signature;

diff -r b0568a9dd160 -r a91e32843310 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Thu Jan 03 16:53:18 2019 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Thu Jan 03 20:16:42 2019 +0100
@@ -164,7 +164,7 @@
     val mfix = map mfix_of type_decls;
     val _ = map2 check_args type_decls mfix;
     val consts = map (fn (t, _, _) => (t, "")) type_decls;
-  in Syntax_Ext.syn_ext (map_filter I mfix) consts ([], [], [], []) ([], []) end;
+  in Syntax_Ext.syn_ext [] (map_filter I mfix) consts ([], [], [], []) ([], []) end;
 
 
 (* syn_ext_consts *)
@@ -215,9 +215,7 @@
           apsnd Syntax_Trans.non_typed_tr' o Syntax_Trans.mk_binder_tr' o swap);
 
     val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
-  in
-    Syntax_Ext.syn_ext' logical_types mfix consts ([], binder_trs, binder_trs', []) ([], [])
-  end;
+  in Syntax_Ext.syn_ext logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) end;
 
 end;
 
diff -r b0568a9dd160 -r a91e32843310 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;